Metamath Proof Explorer - mmtheorems11

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 1001-1100 - Page 11 of 58

Type	Label	Description
Statement
Theorem	ddeeq1 1001	Quantifier introduction when one pair of variables is distinct.
⊢ (¬ ∀x x = y → (y = z → ∀x y = z))
Theorem	ddeeq2 1002	Quantifier introduction when one pair of variables is distinct.
⊢ (¬ ∀x x = y → (z = y → ∀x z = y))
Theorem	ddeel1 1003	Quantifier introduction when one pair of variables is distinct.
⊢ (¬ ∀x x = y → (y ∈ z → ∀x y ∈ z))
Theorem	ddeel2 1004	Quantifier introduction when one pair of variables is distinct.
⊢ (¬ ∀x x = y → (z ∈ y → ∀x z ∈ y))
Theorem	sbal2 1005	Move quantifier in and out of substitution.
⊢ (¬ ∀x x = y → ([z / y]∀xφ ↔ ∀x[z / y]φ))
Theorem	ax15 1006	Axiom ax-15 806 is redundant if we assume ax-17 925. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'.
⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))
Syntax	weu 1007	Extend wff definition to include existential uniqueness ("there exists a unique x such that φ").
wff ∃!xφ
Syntax	wmo 1008	Extend wff definition to include uniqueness ("there exists at most one x such that φ").
wff ∃*xφ
Definition	df-eu 1009	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 1019, eu2 1023, eu3 1024, and eu5 1035 (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 1070).
⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))
Definition	df-mo 1010	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 1027. For other possible definitions see mo2 1026 and mo4 1029.
⊢ (∃*xφ ↔ (∃xφ → ∃!xφ))
Theorem	euf 1011	A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition.
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))
Theorem	bieud 1012	Formula-building rule for uniqueness quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃!xψ ↔ ∃!xχ))
Theorem	bieudv 1013	Formula-building rule for uniqueness quantifier (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃!xψ ↔ ∃!xχ))
Theorem	bieu 1014	Introduce uniqueness quantifier to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃!xφ ↔ ∃!xψ)
Theorem	hbeu1 1015	Bound-variable hypothesis builder for uniqueness.
⊢ (∃!xφ → ∀x∃!xφ)
Theorem	hbeu 1016	Bound-variable hypothesis builder for "at most one". Note that x and y needn't be distinct (this makes the proof more difficult).
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃!yφ → ∀x∃!yφ)
Theorem	sb8eu 1017	Variable substitution in uniqueness quantifier. (This theorem can also be proved without requiring that x and y be distinct, but the proof would be longer.)
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃!xφ ↔ ∃!y[y / x]φ)
Theorem	cbveu 1018	Rule used to change bound variables with implicit substitution.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃!xφ ↔ ∃!yψ)
Theorem	eu1 1019	An alternate way of expressing uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110.
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃!xφ ↔ ∃x(φ ∧ ∀y([y / x]φ → x = y)))
Theorem	mo 1020	Equivalent definitions of "there exists at most one".
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃y∀x(φ → x = y) ↔ ∀x∀y((φ ∧ [y / x]φ) → x = y))
Theorem	euex 1021	Existential uniqueness implies existence.
⊢ (∃!xφ → ∃xφ)
Theorem	eumo0 1022	Existential uniqueness implies "at most one".
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃!xφ → ∃y∀x(φ → x = y))
Theorem	eu2 1023	An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26.
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃!xφ ↔ (∃xφ ∧ ∀x∀y((φ ∧ [y / x]φ) → x = y)))
Theorem	eu3 1024	An alternate way of expressing existential uniqueness.
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃!xφ ↔ (∃xφ ∧ ∃y∀x(φ → x = y)))
Theorem	euorv 1025	Introduction of a disjunct into uniqueness quantifier.
⊢ ((¬ φ ∧ ∃!xψ) → ∃!x(φ ∨ ψ))
Theorem	mo2 1026	Alternate definition of "at most one".
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃*xφ ↔ ∃y∀x(φ → x = y))
Theorem	mo3 1027	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.
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃*xφ ↔ ∀x∀y((φ ∧ [y / x]φ) → x = y))
Theorem	mo4f 1028	"At most one" expressed using implicit substitution.
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃*xφ ↔ ∀x∀y((φ ∧ ψ) → x = y))
Theorem	mo4 1029	"At most one" expressed using implicit substitution.
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃*xφ ↔ ∀x∀y((φ ∧ ψ) → x = y))
Theorem	bimod 1030	Formula-building rule for "at most one" quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃*xψ ↔ ∃*xχ))
Theorem	bimo 1031	Formula-building rule for "at most one" quantifier (inference rule).
⊢ (ψ ↔ χ)    ⇒   ⊢ (∃*xψ ↔ ∃*xχ)
Theorem	hbmo1 1032	Bound-variable hypothesis builder for "at most one".
⊢ (∃*xφ → ∀x∃*xφ)
Theorem	hbmo 1033	Bound-variable hypothesis builder for "at most one".
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃*yφ → ∀x∃*yφ)
Theorem	cbvmo 1034	Rule used to change bound variables with implicit substitution.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃*xφ ↔ ∃*yψ)
Theorem	eu5 1035	Uniqueness in terms of "at most one".
⊢ (∃!xφ ↔ (∃xφ ∧ ∃*xφ))
Theorem	eu4 1036	Uniqueness using implicit substitution.
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃!xφ ↔ (∃xφ ∧ ∀x∀y((φ ∧ ψ) → x = y)))
Theorem	eumo 1037	Existential uniqueness implies "at most one".
⊢ (∃!xφ → ∃*xφ)
Theorem	eumoi 1038	"At most one" inferred from existential uniqueness.
⊢ ∃!xφ    ⇒   ⊢ ∃*xφ
Theorem	exmoeu 1039	Existence in terms of "at most one" and uniqueness.
⊢ (∃xφ ↔ (∃*xφ → ∃!xφ))
Theorem	exmoeu2 1040	Existence implies "at most one" is equivalent to uniqueness.
⊢ (∃xφ → (∃*xφ ↔ ∃!xφ))
Theorem	moabs 1041	Absorption of existence condition by "at most one".
⊢ (∃*xφ ↔ (∃xφ → ∃*xφ))
Theorem	exmo 1042	Something exists or at most one exists.
⊢ (∃xφ ∨ ∃*xφ)
Theorem	immo 1043	"At most one" is preserved through implication (notice wff reversal).
⊢ (∀x(φ → ψ) → (∃*xψ → ∃*xφ))
Theorem	moimv 1044	Move antecedent outside of "at most one".
⊢ (∃*x(φ → ψ) → (φ → ∃*xψ))
Theorem	euimmo 1045	Uniqueness implies "at most one" through implication.
⊢ (∀x(φ → ψ) → (∃!xψ → ∃*xφ))
Theorem	moan 1046	"At most one" is still the case when a conjunct is added.
⊢ (∃*xφ → ∃*x(ψ ∧ φ))
Theorem	moani 1047	"At most one" is still true when a conjunct is added.
⊢ ∃*xφ    ⇒   ⊢ ∃*x(ψ ∧ φ)
Theorem	moor 1048	"At most one" is still the case when a disjunct is removed.
⊢ (∃*x(φ ∨ ψ) → ∃*xφ)
Theorem	mooran1 1049	"At most one" imports disjunction to conjunction.
⊢ ((∃*xφ ∨ ∃*xψ) → ∃*x(φ ∧ ψ))
Theorem	mooran2 1050	"At most one" exports disjunction to conjunction.
⊢ (∃*x(φ ∨ ψ) → (∃*xφ ∧ ∃*xψ))
Theorem	moanim 1051	Introduction of a conjunct into "at most one" quantifier.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃*x(φ ∧ ψ) ↔ (φ → ∃*xψ))
Theorem	moanimv 1052	Introduction of a conjunct into "at most one" quantifier.
⊢ (∃*x(φ ∧ ψ) ↔ (φ → ∃*xψ))
Theorem	euanv 1053	Introduction of a conjunct into uniqueness quantifier.
⊢ (∃!x(φ ∧ ψ) ↔ (φ ∧ ∃!xψ))
Theorem	mopick 1054	"At most one" picks a variable value, eliminating an existential quantifier.
⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ))
Theorem	eupick 1055	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, which apparently does not appear explicitly in the literature, can be quite useful because it lets us eliminate existential quantifiers in a hypothesis.
⊢ ((∃!xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ))
Theorem	eupickb 1056	Existential uniqueness "pick" showing wff equivalence.
⊢ ((∃!xφ ∧ ∃!xψ ∧ ∃x(φ ∧ ψ)) → (φ ↔ ψ))
Theorem	mopick2 1057	"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 773.
⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → ∃x(φ ∧ ψ ∧ χ))
Theorem	moexex 1058	"At most one" double quantification.
⊢ (φ → ∀yφ)    ⇒   ⊢ ((∃*xφ ∧ ∀x∃*yψ) → ∃*y∃x(φ ∧ ψ))
Theorem	moexexv 1059	"At most one" double quantification.
⊢ ((∃*xφ ∧ ∀x∃*yψ) → ∃*y∃x(φ ∧ ψ))
Theorem	2moex 1060	Double quantification with "at most one".
⊢ (∃*x∃yφ → ∀y∃*xφ)
Theorem	2euex 1061	Double quantification with existential uniqueness.
⊢ (∃!x∃yφ → ∃y∃!xφ)
Theorem	2eumo 1062	Double quantification with existential uniqueness and "at most one".
⊢ (∃!x∃*yφ → ∃*x∃!yφ)
Theorem	2eu2ex 1063	Double existential uniqueness.
⊢ (∃!x∃!yφ → ∃x∃yφ)
Theorem	2moswap 1064	A condition allowing swap of "at most one" and existential quantifiers.
⊢ (∀x∃*yφ → (∃*x∃yφ → ∃*y∃xφ))
Theorem	2euswap 1065	A condition allowing swap of uniqueness and existential quantifiers.
⊢ (∀x∃*yφ → (∃!x∃yφ → ∃!y∃xφ))
Theorem	2exeu 1066	Double existential uniqueness implies double uniqueness quantification.
⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) → ∃!x∃!yφ)
Theorem	2eu1 1067	Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one.
⊢ (∀x∃*yφ → (∃!x∃!yφ ↔ (∃!x∃yφ ∧ ∃!y∃xφ)))
Theorem	2eu2 1068	Double existential uniqueness.
⊢ (∃!y∃xφ → (∃!x∃!yφ ↔ ∃!x∃yφ))
Theorem	2eu3 1069	Double existential uniqueness.
⊢ (∀x∀y(∃*xφ ∨ ∃*yφ) → ((∃!x∃!yφ ∧ ∃!y∃!xφ) ↔ (∃!x∃yφ ∧ ∃!y∃xφ)))
Theorem	2eu4 1070	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 1067 for a condition under which the naive definition holds and 2exeu 1066 for a one-way implication. See 2eu5 1071 for an alternate definition.
⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ (∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (x = z ∧ y = w))))
Theorem	2eu5 1071	An alternate definition of double existential uniqueness (see 2eu4 1070). 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.")
⊢ ((∃!x∃!yφ ∧ ∀x∃*yφ) ↔ (∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (x = z ∧ y = w))))
Theorem	exists1 1072	Two ways of expressing "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 1889.
⊢ (∃!x x = x ↔ ∀x x = y)
Theorem	exists2 1073	A condition implying that at least two things exist.
⊢ ((∃xφ ∧ ∃x ¬ φ) → ¬ ∃!x x = x)
Axiom	ax-ext 1074	Axiom of Extensionality. An axiom of Zermelo-Fraenkel set theory. It states that two sets are identical if they contain the same elements. Axiom Ext of [BellMachover] p. 461. Set theory can also be formulated with a single primitive predicate ∈ on top of traditional predicate calculus without equality. In that case the Axiom of Extensionality becomes (∀w(w ∈ x ↔ w ∈ y) → (x ∈ z → y ∈ z)), and equality x = y is defined as ∀w(w ∈ x ↔ w ∈ y). All of the usual axioms of equality then become theorems of set theory. See, for example, Axiom 1 of [TakeutiZaring] p. 8. To use this version of Extensionality with Metamath's logical axioms, on the other hand, we could delete from them ax-8 798 through ax-16 922, leaving only the beautifully simple ax-4 673 through ax-7 676 (and ax-gen 677), and those that we couldn't prove as theorems we would add back as additional axioms of set theory. Or should they still be considered part of "logic" proper? I suppose this is a philosophical issue. Under traditional predicate calculus, this version of Extensionality moves the properties of equality into set theory, and it can be argued that proper substitution - which is broken out explicitly in the Metamath axioms - has an intimate tie-in with equality that is implicitly "hidden" in the traditional axioms of predicate calculus. The axiomatics of such a system - i.e. devising simple, elegant axioms - have apparently never been studied nor even considered. (Perhaps some day I will play with it if no one else does.)
⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y)
Axiom	ax-rep 1075	Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory. Axiom 5 of [TakeutiZaring] p. 19. It tells us that that the image of any set under a function is also a set (see the variant funimaex 2716). Although φ may be any wff whatsoever, this axiom is useful (i.e. its antecedent is satisfied) when we are given some function and φ encodes the predicate "the value of the function at w is z". Thus φ will ordinarily have free variables w and z - think of it informally as φ(w, z). We prefix φ with the quantifier ∀y in order to "protect" the axiom from any φ containing y, thus allowing us to eliminate any restrictions on φ. This makes the axiom usable in a formalization that omits the logically redundant axiom ax-17 925. Another common variant is derived as zfrep3 1476, where you can find some further remarks. A slightly more compact version is shown as axrep 1473. A quite different variant is zfrep6 2744, which if used in place of ax-rep 1075 would also require that the Separation Scheme zfaus 1480 be stated as a separate axiom. There is very a strong generalization of Replacement that doesn't demand function-like behavior of φ. Two versions of this generalization are called the Collection Principle cp 3547 and the Boundedness Axiom bnd 3548. The Collection Principle is sometimes used in place of Replacement as one of the ZF axioms, for example at MathWorld http://mathworld.wolfram.com/Zermelo-FraenkelAxioms.html where it is (somewhat misleadingly) called "Replacement".
⊢ (∀w∃y∀z(∀yφ → z = y) → ∃y∀z(z ∈ y ↔ ∃w(w ∈ x ∧ ∀yφ)))
Axiom	ax-un 1076	Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states that the union of any set exists. A variant is Axiom Union of [BellMachover] p. 466 (which can be derived from this version using bm1.3ii 1481). A version using abbreviations is uniex 1947.
⊢ ∃y∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y)
Axiom	ax-pow 1077	Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory. It states that the collection of all subsets of a set is also a set. A variant is Axiom Pow of [BellMachover] p. 466 (which can be derived from this version using bm1.3ii 1481). A version using abbreviations is pwex 1806.
⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)
Axiom	ax-reg 1078	Axiom of Regularity. An axiom of Zermelo-Fraenkel set theory. Also called the Axiom of Foundation. A rather non-intuitive axiom that denies more than it asserts, it states (in the form of zfreg 3447) that every non-empty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (eirrv 3449). A stronger version that works for proper classes is proved as zfregs 3491.
⊢ (∃y y ∈ x → ∃y(y ∈ x ∧ ∀z(z ∈ y → ¬ z ∈ x)))
Axiom	ax-inf 1079	Axiom of Infinity. An axiom of Zermelo-Fraenkel set theory. This axiom is the gateway to "Cantor's paradise" (an expression coined by Hilbert). The axiom asserts that an infinite set exists, or more specifically, "there exists a non-empty set that is a subset of its union." Our version is not common the literature, but a proof that it implies the more standard version is given by inf3 3471. Its advantage is that when expanded to primitives, it uses fewer symbols than the standard version. Our version is a slight variant of the Axiom of Infinity in [FreydScedrov] p. 283, proved here as inf1 3458. Variants of the standard version are zfinf 3474 (which is Axiom Inf of [BellMachover] p. 472) and omex 3475 (Axiom 7 of [TakeutiZaring] p. 43). The standard version essentially states that there exists a set containing all the natural numbers. Theorem inf0 3457 shows the reverse derivation of our axiom from a standard one. Theorem inf5 3472 shows a very short way to state this axiom.
⊢ ∃y(x ∈ y ∧ ∀z(z ∈ y → ∃w(z ∈ w ∧ w ∈ y)))
Axiom	ax-ac 1080	Axiom of Choice. The Axiom of Choice (AC) is usually considered an extension of ZF set theory rather than a proper part of it. It is sometimes considered philosophically controversial because it asserts the existence of a set without telling us what the set is. ZF set theory that includes AC is called ZFC. AC (in a common version given in textbooks) asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. Stated another way, there exists a "choice function" on any set that maps each (non-empty) member of the set to an arbitrary member of that member. The unpublished version shown here was specifically crafted to be short when expanded to primitives and may be the shortest possible (although Kurt Maes' 5-quantifier formula ackm 3597 is the same length when the biconditional of ax-ac 1080 is expanded). In order to understand ax-ac 1080, you should look at the rewritten version ac3 3568, which is accompanied by an informal explanation. Standard textbook versions of AC are derived as ac4 3571 and ac5 3573 (which is Axiom AC of [BellMachover] p. 488). The Axiom of Regularity ax-reg 1078 (among others) is used to derive our version from the standard ones; this reverse derivation is shown as theorem aceq6b 3565. Equivalents to AC are the well-ordering theorem weth 3602 and Zorn's lemma zorn2 3612.
⊢ ∃y∀z∀w((z ∈ w ∧ w ∈ x) → ∃v∀u(∃t((u ∈ w ∧ w ∈ t) ∧ (u ∈ t ∧ t ∈ y)) ↔ u = v))
Theorem	axun 1081	Axiom of Union expressed with fewest number of different variables.
⊢ ∃x∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x)
Theorem	axpow 1082	Axiom of Power Sets expressed with fewest number of different variables.
⊢ ∃x∀y(∀x(x ∈ y → x ∈ z) → y ∈ x)
Theorem	axreg 1083	Axiom of Regularity expressed more compactly.
⊢ (x ∈ y → ∃x(x ∈ y ∧ ∀z(z ∈ x → ¬ z ∈ y)))
Theorem	axinf 1084	Axiom of Infinity expressed with fewest number of different variables.
⊢ ∃x(y ∈ x ∧ ∀y(y ∈ x → ∃z(y ∈ z ∧ z ∈ x)))
Theorem	axac 1085	Axiom of Choice expressed with fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac 1080.
⊢ ∃x∀y∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))
Theorem	axext 1086	The Axiom of Extensionality (ax-ext 1074) restated so that it postulates the existence of a set z given two arbitrary sets x and y. This way of expressing it follows the general idea of the other ZFC axioms, which is to postulate the existence of sets given other sets.
⊢ ∃z((z ∈ x ↔ z ∈ y) → x = y)
Theorem	zfext2 1087	A generalization of the Axiom of Extensionality in which x and y need not be distinct.
⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y)
Theorem	bm1.1 1088	Any set which has a property is the only set with that property. Theorem 1.1 of [BellMachover] p. 462.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃x∀y(y ∈ x ↔ φ) → ∃!x∀y(y ∈ x ↔ φ))
Syntax	cv 1089	All sets are classes (but not vice-versa!).
class x
Syntax	cab 1090	Introduce class abstraction notation ('the class of sets x such that φ is true'). Some classes defined with this notation are not sets, i.e. do not exist.
class {x∣φ}
Syntax	wceq 1091	Extend wff definition to include class equality.
wff A = B
Syntax	wcel 1092	Extend wff definition to include the membership connective between classes.
wff A ∈ B
Definition	df-clab 1093	Define the class abstraction, also called "set builder" notation in the literature. x and y need not be distinct. Definition 2.1 of [Quine] p. 16. Typically, φ will have y as a free variable, and "{y∣φ}" is read "the class of all sets y such that φ(y) is true." We do not define {y∣φ} in isolation but only as part of an expression that extends or "overloads" the ∈ relationship. This is our first use of the ∈ symbol to connect classes instead of sets. The syntax definition wcel 1092, which extends or "overloads" the wel 803 definition connecting set variables, requires that both sides of ∈ be a class. In the present definition, the x on the left-hand side is a set variable. We use the syntax definition cv 1089 to "convert" the set variable x to a class term: all sets are classes (but not necessarily vice-versa). In df-cleq 1097 and df-clel 1099 we introduce a new kind of variable (class variable) that can substituted with expressions such as {y∣φ}. For a full description of how classes are introduced and how to recover the primitive language, see the discussion in Quine (and under cleqab 1174 for a quick overview). Because class variables can be substituted with compound expressions and set variables cannot, it is often useful to convert a theorem containing a free set variable to a more general version with a class variable. This is done with theorems such as vtoclg 1383 which is used, for example, to convert eirrv 3449 to eirr 3450.
⊢ (x ∈ {y∣φ} ↔ [x / y]φ)
Theorem	abid 1094	Simplification of class abstraction notation when the free and bound variables are identical.
⊢ (x ∈ {x∣φ} ↔ φ)
Theorem	hbab1 1095	The abstraction variable in an class abstraction is not free.
⊢ (y ∈ {x∣φ} → ∀x y ∈ {x∣φ})
Theorem	hbab 1096	A variable not free in a wff remains so in an class abstraction.
⊢ (φ → ∀xφ)    ⇒   ⊢ (z ∈ {y∣φ} → ∀x z ∈ {y∣φ})
Definition	df-cleq 1097	Define the equality connective between classes. Definition 2.7 of [Quine] p. 18. Also Definition 4.5 of [TakeutiZaring] p. 13; Chapter 4 provides its justification and methods for eliminating it. Note that its elimination will not necessarily result in a single wff in the original language but possibly a "scheme" of wffs. This is an example of a somewhat "risky" definition, because it extends the use of the existing equality symbol rather than introducing a new symbol, allowing us to make statements in the original language that may not be true. For example, it permits us to deduce y = z ↔ ∀x(x ∈ y ↔ x ∈ z) which is not a theorem of logic but rather presupposes the Axiom of Extensionality, which we must therefore include as a hypothesis. We could avoid the danger by introducing another symbol, say == , in place of =; this would also have the advantage of making elimination of the definition straightforward, so that we could eliminate Extensionality as a hypothesis. We would then also have the advantage of being able to identify in various proofs exactly where Extensionality truly comes into play. Then, one of our theorems would then be x == y ↔ x = y by invoking Extensionality. However in keeping with standard practice we retain the "dangerous" definition; this also makes some proofs shorter. See also comments under df-clab 1093, df-clel 1099, and cleqab 1174.
⊢ (∀x(x ∈ y ↔ x ∈ z) → y = z)    ⇒   ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
Theorem	dfcleq 1098	The same as df-cleq 1097 with the hypothesis removed using the Axiom of Extensionality ax-ext 1074.
⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
Definition	df-clel 1099	Define the membership connective between classes. Theorem 6.3 of [Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we adopt as a definition. See these references for its metalogical justification. Note that like df-cleq 1097 it extends or "overloads" the use of the existing membership symbol, but unlike df-cleq 1097 it does not strengthen the set of valid wffs of logic when the class variables are replaced with set variables (see cleljust 985), so we don't include any set theory axiom as a hypothesis. See also comments about the syntax under df-clab 1093.
⊢ (A ∈ B ↔ ∃x(x = A ∧ x ∈ B))
Theorem	cleqrd 1100	Deduce equality of sets from equivalence of membership.
⊢ (φ → (x ∈ A ↔ x ∈ B))    ⇒   ⊢ (φ → A = B)