HomeHome New Foundations Explorer
Theorem List (p. 23 of 64)
< Previous  Next >
Bad symbols? Use Firefox
(or GIF version for IE).

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 2201-2300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremax11v2-o 2201* Recovery of ax-11o 2141 from ax11v 2096 without using ax-11o 2141. The hypothesis is even weaker than ax11v 2096, with z both distinct from x and not occurring in φ. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-11o 2141. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
(x = z → (φx(x = zφ)))       x x = y → (x = y → (φx(x = yφ))))
 
Theoremax11a2-o 2202* Derive ax-11o 2141 from a hypothesis in the form of ax-11 1746, without using ax-11 1746 or ax-11o 2141. The hypothesis is even weaker than ax-11 1746, with z both distinct from x and not occurring in φ. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-11 1746, if we also hvae ax-10o 2139 which this proof uses . As theorem ax11 2155 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-10 2140 instead of ax-10o 2139. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
(x = z → (zφx(x = zφ)))       x x = y → (x = y → (φx(x = yφ))))
 
Theoremax10o-o 2203 Show that ax-10o 2139 can be derived from ax-10 2140. An open problem is whether this theorem can be derived from ax-10 2140 and the others when ax-11 1746 is replaced with ax-11o 2141. See theorem ax10from10o 2177 for the rederivation of ax-10 2140 from ax10o 1952.

Normally, ax10o 1952 should be used rather than ax-10o 2139 or ax10o-o 2203, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

(x x = y → (xφyφ))
 
1.7  Existential uniqueness
 
Syntaxweu 2204 Extend wff definition to include existential uniqueness ("there exists a unique x such that φ").
wff ∃!xφ
 
Syntaxwmo 2205 Extend wff definition to include uniqueness ("there exists at most one x such that φ").
wff ∃*xφ
 
Theoremeujust 2206* A soundness justification theorem for df-eu 2208, showing that the definition is equivalent to itself with its dummy variable renamed. Note that y and z needn't be distinct variables. See eujustALT 2207 for a proof that provides an example of how it can be achieved through the use of dvelim 2016. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(yx(φx = y) ↔ zx(φx = z))
 
TheoremeujustALT 2207* A soundness justification theorem for df-eu 2208, showing that the definition is equivalent to itself with its dummy variable renamed. Note that y and z needn't be distinct variables. While this isn't strictly necessary for soundness, the proof provides an example of how it can be achieved through the use of dvelim 2016. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
(yx(φx = y) ↔ zx(φx = z))
 
Definitiondf-eu 2208* Define existential uniqueness, i.e. "there exists exactly one x such that φ." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2225, eu2 2229, eu3 2230, and eu5 2242 (which in some cases we show with a hypothesis φyφ in place of a distinct variable condition on y and φ). Double uniqueness is tricky: ∃!x∃!yφ does not mean "exactly one x and one y " (see 2eu4 2287). (Contributed by NM, 12-Aug-1993.)
(∃!xφyx(φx = y))
 
Definitiondf-mo 2209 Define "there exists at most one x such that φ." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2235. For other possible definitions see mo2 2233 and mo4 2237. (Contributed by NM, 8-Mar-1995.)
(∃*xφ ↔ (xφ∃!xφ))
 
Theoremeuf 2210* A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.)
yφ       (∃!xφyx(φx = y))
 
Theoremeubid 2211 Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
xφ    &   (φ → (ψχ))       (φ → (∃!xψ∃!xχ))
 
Theoremeubidv 2212* Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
(φ → (ψχ))       (φ → (∃!xψ∃!xχ))
 
Theoremeubii 2213 Introduce uniqueness quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
(φψ)       (∃!xφ∃!xψ)
 
Theoremnfeu1 2214 Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
x∃!xφ
 
Theoremnfmo1 2215 Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
x∃*xφ
 
Theoremnfeud2 2216 Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.)
yφ    &   ((φ ¬ x x = y) → Ⅎxψ)       (φ → Ⅎx∃!yψ)
 
Theoremnfmod2 2217 Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.)
yφ    &   ((φ ¬ x x = y) → Ⅎxψ)       (φ → Ⅎx∃*yψ)
 
Theoremnfeud 2218 Deduction version of nfeu 2220. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)
yφ    &   (φ → Ⅎxψ)       (φ → Ⅎx∃!yψ)
 
Theoremnfmod 2219 Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
yφ    &   (φ → Ⅎxψ)       (φ → Ⅎx∃*yψ)
 
Theoremnfeu 2220 Bound-variable hypothesis builder for "at most one." Note that x and y needn't be distinct (this makes the proof more difficult). (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
xφ       x∃!yφ
 
Theoremnfmo 2221 Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
xφ       x∃*yφ
 
Theoremsb8eu 2222 Variable substitution in uniqueness quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
yφ       (∃!xφ∃!y[y / x]φ)
 
Theoremsb8mo 2223 Variable substitution in uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
yφ       (∃*xφ∃*y[y / x]φ)
 
Theoremcbveu 2224 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
yφ    &   xψ    &   (x = y → (φψ))       (∃!xφ∃!yψ)
 
Theoremeu1 2225* An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
yφ       (∃!xφx(φ y([y / x]φx = y)))
 
Theoremmo 2226* Equivalent definitions of "there exists at most one." (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
yφ       (yx(φx = y) ↔ xy((φ [y / x]φ) → x = y))
 
Theoremeuex 2227 Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(∃!xφxφ)
 
Theoremeumo0 2228* Existential uniqueness implies "at most one." (Contributed by NM, 8-Jul-1994.)
yφ       (∃!xφyx(φx = y))
 
Theoremeu2 2229* An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.)
yφ       (∃!xφ ↔ (xφ xy((φ [y / x]φ) → x = y)))
 
Theoremeu3 2230* An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.)
yφ       (∃!xφ ↔ (xφ yx(φx = y)))
 
Theoremeuor 2231 Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.)
xφ       ((¬ φ ∃!xψ) → ∃!x(φ ψ))
 
Theoremeuorv 2232* Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
((¬ φ ∃!xψ) → ∃!x(φ ψ))
 
Theoremmo2 2233* Alternate definition of "at most one." (Contributed by NM, 8-Mar-1995.)
yφ       (∃*xφyx(φx = y))
 
Theoremsbmo 2234* Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
([y / x]∃*zφ∃*z[y / x]φ)
 
Theoremmo3 2235* Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that y not occur in φ in place of our hypothesis. (Contributed by NM, 8-Mar-1995.)
yφ       (∃*xφxy((φ [y / x]φ) → x = y))
 
Theoremmo4f 2236* "At most one" expressed using implicit substitution. (Contributed by NM, 10-Apr-2004.)
xψ    &   (x = y → (φψ))       (∃*xφxy((φ ψ) → x = y))
 
Theoremmo4 2237* "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
(x = y → (φψ))       (∃*xφxy((φ ψ) → x = y))
 
Theoremmobid 2238 Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.)
xφ    &   (φ → (ψχ))       (φ → (∃*xψ∃*xχ))
 
Theoremmobidv 2239* Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)
(φ → (ψχ))       (φ → (∃*xψ∃*xχ))
 
Theoremmobii 2240 Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
(ψχ)       (∃*xψ∃*xχ)
 
Theoremcbvmo 2241 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.)
yφ    &   xψ    &   (x = y → (φψ))       (∃*xφ∃*yψ)
 
Theoremeu5 2242 Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.)
(∃!xφ ↔ (xφ ∃*xφ))
 
Theoremeu4 2243* Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)
(x = y → (φψ))       (∃!xφ ↔ (xφ xy((φ ψ) → x = y)))
 
Theoremeumo 2244 Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
(∃!xφ∃*xφ)
 
Theoremeumoi 2245 "At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
∃!xφ       ∃*xφ
 
Theoremexmoeu 2246 Existence in terms of "at most one" and uniqueness. (Contributed by NM, 5-Apr-2004.)
(xφ ↔ (∃*xφ∃!xφ))
 
Theoremexmoeu2 2247 Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.)
(xφ → (∃*xφ∃!xφ))
 
Theoremmoabs 2248 Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.)
(∃*xφ ↔ (xφ∃*xφ))
 
Theoremexmo 2249 Something exists or at most one exists. (Contributed by NM, 8-Mar-1995.)
(xφ ∃*xφ)
 
Theoremmoim 2250 "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 22-Apr-1995.)
(x(φψ) → (∃*xψ∃*xφ))
 
Theoremmoimi 2251 "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
(φψ)       (∃*xψ∃*xφ)
 
Theoremmorimv 2252* Move antecedent outside of "at most one." (Contributed by NM, 28-Jul-1995.)
(∃*x(φψ) → (φ∃*xψ))
 
Theoremeuimmo 2253 Uniqueness implies "at most one" through implication. (Contributed by NM, 22-Apr-1995.)
(x(φψ) → (∃!xψ∃*xφ))
 
Theoremeuim 2254 Add existential uniqueness quantifiers to an implication. Note the reversed implication in the antecedent. (Contributed by NM, 19-Oct-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
((xφ x(φψ)) → (∃!xψ∃!xφ))
 
Theoremmoan 2255 "At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.)
(∃*xφ∃*x(ψ φ))
 
Theoremmoani 2256 "At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.)
∃*xφ       ∃*x(ψ φ)
 
Theoremmoor 2257 "At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.)
(∃*x(φ ψ) → ∃*xφ)
 
Theoremmooran1 2258 "At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
((∃*xφ ∃*xψ) → ∃*x(φ ψ))
 
Theoremmooran2 2259 "At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(∃*x(φ ψ) → (∃*xφ ∃*xψ))
 
Theoremmoanim 2260 Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 3-Dec-2001.)
xφ       (∃*x(φ ψ) ↔ (φ∃*xψ))
 
Theoremeuan 2261 Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
xφ       (∃!x(φ ψ) ↔ (φ ∃!xψ))
 
Theoremmoanimv 2262* Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
(∃*x(φ ψ) ↔ (φ∃*xψ))
 
Theoremmoaneu 2263 Nested "at most one" and uniqueness quantifiers. (Contributed by NM, 25-Jan-2006.)
∃*x(φ ∃!xφ)
 
Theoremmoanmo 2264 Nested "at most one" quantifiers. (Contributed by NM, 25-Jan-2006.)
∃*x(φ ∃*xφ)
 
Theoremeuanv 2265* Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
(∃!x(φ ψ) ↔ (φ ∃!xψ))
 
Theoremmopick 2266 "At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997.)
((∃*xφ x(φ ψ)) → (φψ))
 
Theoremeupick 2267 Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing x such that φ is true, and there is also an x (actually the same one) such that φ and ψ are both true, then φ implies ψ regardless of x. This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by NM, 10-Jul-1994.)
((∃!xφ x(φ ψ)) → (φψ))
 
Theoremeupicka 2268 Version of eupick 2267 with closed formulas. (Contributed by NM, 6-Sep-2008.)
((∃!xφ x(φ ψ)) → x(φψ))
 
Theoremeupickb 2269 Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994.)
((∃!xφ ∃!xψ x(φ ψ)) → (φψ))
 
Theoremeupickbi 2270 Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∃!xφ → (x(φ ψ) ↔ x(φψ)))
 
Theoremmopick2 2271 "At most one" can show the existence of a common value. In this case we can infer existence of conjunction from a conjunction of existence, and it is one way to achieve the converse of 19.40 1609. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
((∃*xφ x(φ ψ) x(φ χ)) → x(φ ψ χ))
 
Theoremeuor2 2272 Introduce or eliminate a disjunct in a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
xφ → (∃!x(φ ψ) ↔ ∃!xψ))
 
Theoremmoexex 2273 "At most one" double quantification. (Contributed by NM, 3-Dec-2001.)
yφ       ((∃*xφ x∃*yψ) → ∃*yx(φ ψ))
 
Theoremmoexexv 2274* "At most one" double quantification. (Contributed by NM, 26-Jan-1997.)
((∃*xφ x∃*yψ) → ∃*yx(φ ψ))
 
Theorem2moex 2275 Double quantification with "at most one." (Contributed by NM, 3-Dec-2001.)
(∃*xyφy∃*xφ)
 
Theorem2euex 2276 Double quantification with existential uniqueness. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(∃!xyφy∃!xφ)
 
Theorem2eumo 2277 Double quantification with existential uniqueness and "at most one." (Contributed by NM, 3-Dec-2001.)
(∃!x∃*yφ∃*x∃!yφ)
 
Theorem2eu2ex 2278 Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
(∃!x∃!yφxyφ)
 
Theorem2moswap 2279 A condition allowing swap of "at most one" and existential quantifiers. (Contributed by NM, 10-Apr-2004.)
(x∃*yφ → (∃*xyφ∃*yxφ))
 
Theorem2euswap 2280 A condition allowing swap of uniqueness and existential quantifiers. (Contributed by NM, 10-Apr-2004.)
(x∃*yφ → (∃!xyφ∃!yxφ))
 
Theorem2exeu 2281 Double existential uniqueness implies double uniqueness quantification. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Mario Carneiro, 22-Dec-2016.)
((∃!xyφ ∃!yxφ) → ∃!x∃!yφ)
 
Theorem2mo 2282* Two equivalent expressions for double "at most one." (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)
(zwxy(φ → (x = z y = w)) ↔ xyzw((φ [z / x][w / y]φ) → (x = z y = w)))
 
Theorem2mos 2283* Double "exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005.)
((x = z y = w) → (φψ))       (zwxy(φ → (x = z y = w)) ↔ xyzw((φ ψ) → (x = z y = w)))
 
Theorem2eu1 2284 Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. (Contributed by NM, 3-Dec-2001.)
(x∃*yφ → (∃!x∃!yφ ↔ (∃!xyφ ∃!yxφ)))
 
Theorem2eu2 2285 Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
(∃!yxφ → (∃!x∃!yφ∃!xyφ))
 
Theorem2eu3 2286 Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
(xy(∃*xφ ∃*yφ) → ((∃!x∃!yφ ∃!y∃!xφ) ↔ (∃!xyφ ∃!yxφ)))
 
Theorem2eu4 2287* This theorem provides us with a definition of double existential uniqueness ("exactly one x and exactly one y"). Naively one might think (incorrectly) that it could be defined by ∃!x∃!yφ. See 2eu1 2284 for a condition under which the naive definition holds and 2exeu 2281 for a one-way implication. See 2eu5 2288 and 2eu8 2291 for alternate definitions. (Contributed by NM, 3-Dec-2001.)
((∃!xyφ ∃!yxφ) ↔ (xyφ zwxy(φ → (x = z y = w))))
 
Theorem2eu5 2288* An alternate definition of double existential uniqueness (see 2eu4 2287). A mistake sometimes made in the literature is to use ∃!x∃!y to mean "exactly one x and exactly one y." (For example, see Proposition 7.53 of [TakeutiZaring] p. 53.) It turns out that this is actually a weaker assertion, as can be seen by expanding out the formal definitions. This theorem shows that the erroneous definition can be repaired by conjoining x∃*yφ as an additional condition. The correct definition apparently has never been published. (∃* means "exists at most one.") (Contributed by NM, 26-Oct-2003.)
((∃!x∃!yφ x∃*yφ) ↔ (xyφ zwxy(φ → (x = z y = w))))
 
Theorem2eu6 2289* Two equivalent expressions for double existential uniqueness. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)
((∃!xyφ ∃!yxφ) ↔ zwxy(φ ↔ (x = z y = w)))
 
Theorem2eu7 2290 Two equivalent expressions for double existential uniqueness. (Contributed by NM, 19-Feb-2005.)
((∃!xyφ ∃!yxφ) ↔ ∃!x∃!y(xφ yφ))
 
Theorem2eu8 2291 Two equivalent expressions for double existential uniqueness. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!x∃!y using 2eu7 2290. (Contributed by NM, 20-Feb-2005.)
(∃!x∃!y(xφ yφ) ↔ ∃!x∃!y(∃!xφ yφ))
 
Theoremeuequ1 2292* Equality has existential uniqueness. Special case of eueq1 3009 proved using only predicate calculus. (Contributed by Stefan Allan, 4-Dec-2008.)
∃!x x = y
 
Theoremexists1 2293* Two ways to express "only one thing exists." The left-hand side requires only one variable to express this. Both sides are false in set theory; see theorem dtru (future). (Contributed by NM, 5-Apr-2004.)
(∃!x x = xx x = y)
 
Theoremexists2 2294 A condition implying that at least two things exist. (Contributed by NM, 10-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
((xφ x ¬ φ) → ¬ ∃!x x = x)
 
1.8  Other axiomatizations related to classical predicate calculus
 
1.8.1  Predicate calculus with all distinct variables
 
Axiomax-7d 2295* Distinct variable version of ax-7 1734. (Contributed by Mario Carneiro, 14-Aug-2015.)
(xyφyxφ)
 
Axiomax-8d 2296* Distinct variable version of ax-8 1675. (Contributed by Mario Carneiro, 14-Aug-2015.)
(x = y → (x = zy = z))
 
Axiomax-9d1 2297 Distinct variable version of ax9 1949, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
¬ x ¬ x = x
 
Axiomax-9d2 2298* Distinct variable version of ax9 1949, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
¬ x ¬ x = y
 
Axiomax-10d 2299* Distinct variable version of ax10 1944. (Contributed by Mario Carneiro, 14-Aug-2015.)
(x x = yy y = x)
 
Axiomax-11d 2300* Distinct variable version of ax-11 1746. (Contributed by Mario Carneiro, 14-Aug-2015.)
(x = y → (yφx(x = yφ)))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6308
  Copyright terms: Public domain < Previous  Next >