Metamath Proof Explorer - mmtheorems15

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 - 1401-1500 - Page 15 of 58

Type	Label	Description
Statement
Theorem	cla4ev 1401	Existential specialization with implicit substitution.
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (ψ → ∃xφ)
Theorem	rcla4v 1402	Restricted specialization with implicit substitution.
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ B φ → (A ∈ B → ψ))
Theorem	rcla4ev 1403	Restricted existential specialization with implicit substitution.
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ B ∧ ψ) → ∃x ∈ B φ)
Theorem	rcla42v 1404	2-variable restricted specialization with implicit substitution.
⊢ (x = A → (φ ↔ χ))    &   ⊢ (y = B → (χ ↔ ψ))    ⇒   ⊢ (∀x ∈ C ∀y ∈ D φ → ((A ∈ C ∧ B ∈ D) → ψ))
Theorem	rcla42ev 1405	2-variable restricted existential specialization with implicit substitution.
⊢ (x = A → (φ ↔ χ))    &   ⊢ (y = B → (χ ↔ ψ))    ⇒   ⊢ (((A ∈ C ∧ B ∈ D) ∧ ψ) → ∃x ∈ C ∃y ∈ D φ)
Theorem	cla4e2v 1406	Existential specialization with implicit substitution.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ (ψ → ∃x∃yφ)
Theorem	eqvinc 1407	A variable introduction law for class equality.
⊢ A ∈ V    ⇒   ⊢ (A = B ↔ ∃x(x = A ∧ x = B))
Theorem	eqvincf 1408	A variable introduction law for class equality, requiring only that x not be free in A and B (instead of not occurring in them).
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    &   ⊢ A ∈ V    ⇒   ⊢ (A = B ↔ ∃x(x = A ∧ x = B))
Theorem	alexeq 1409	Two ways of expressing substitution of A for x in φ.
⊢ A ∈ V    ⇒   ⊢ (∀x(x = A → φ) ↔ ∃x(x = A ∧ φ))
Theorem	ceqex 1410	Equality implies equivalence with substitution.
⊢ (x = A → (φ ↔ ∃x(x = A ∧ φ)))
Theorem	ceqsexg 1411	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis.
⊢ (ψ → ∀xψ)    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (∃x(x = A ∧ φ) ↔ ψ))
Theorem	ceqsexgv 1412	Elimination of an existential quantifier, using implicit substitution.
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (∃x(x = A ∧ φ) ↔ ψ))
Theorem	ceqsrexv 1413	Elimination of a restricted existential quantifier, using implicit substitution.
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (∃x ∈ B (x = A ∧ φ) ↔ ψ))
Theorem	elabf 1414	Membership in a class abstraction with implicit substitution.
⊢ (ψ → ∀xψ)    &   ⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x∣φ} ↔ ψ)
Theorem	elab 1415	Membership in a class abstraction with implicit substitution. Compare Theorem 6.13 of [Quine] p. 44.
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x∣φ} ↔ ψ)
Theorem	elabgf 1416	Membership in a class abstraction with implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. This version has bound variable hypotheses in place of distinct variable restrictions.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (A ∈ {x∣φ} ↔ ψ))
Theorem	elabg 1417	Membership in a class abstraction with implicit substitution. Compare Theorem 6.13 of [Quine] p. 44.
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (A ∈ {x∣φ} ↔ ψ))
Theorem	elab2g 1418	Membership in a class abstraction, using implicit substitution.
⊢ (x = A → (φ ↔ ψ))    &   ⊢ B = {x∣φ}    ⇒   ⊢ (A ∈ C → (A ∈ B ↔ ψ))
Theorem	elab2 1419	Membership in a class abstraction, using implicit substitution.
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ B = {x∣φ}    ⇒   ⊢ (A ∈ B ↔ ψ)
Theorem	elab3g 1420	Membership in a class abstraction using implicit substitution.
⊢ (ψ → A ∈ V)    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x∣φ} ↔ ψ)
Theorem	elrabf 1421	Membership in a restricted class abstraction with implicit substitution. This version has bound variable hypotheses in place of distinct variable restrictions.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x ∈ B∣φ} ↔ (A ∈ B ∧ ψ))
Theorem	elrab 1422	Membership in a restricted class abstraction with implicit substitution.
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x ∈ B∣φ} ↔ (A ∈ B ∧ ψ))
Theorem	cbvab 1423	Rule used to change bound variables with implicit substitution.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ {x∣φ} = {y∣ψ}
Theorem	cbvabv 1424	Rule used to change bound variables with implicit substitution.
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ {x∣φ} = {y∣ψ}
Theorem	cbvrab 1425	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound variable hypotheses in place of distinct variable conditions.
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ A → ∀y z ∈ A)    &   ⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ {x ∈ A∣φ} = {y ∈ A∣ψ}
Theorem	cbvrabv 1426	Rule to change the bound variable in a restricted class abstraction, using implicit substitution.
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ {x ∈ A∣φ} = {y ∈ A∣ψ}
Theorem	eueq 1427	Equality has existential uniqueness.
⊢ (A ∈ V ↔ ∃!x x = A)
Theorem	eueq1 1428	Equality has existential uniqueness.
⊢ A ∈ V    ⇒   ⊢ ∃!x x = A
Theorem	eueq2 1429	Equality has existential uniqueness (split into 2 cases).
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∃!x((φ ∧ x = A) ∨ (¬ φ ∧ x = B))
Theorem	eueq3 1430	Equality has existential uniqueness (split into 3 cases).
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ ¬ (φ ∧ ψ)    ⇒   ⊢ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))
Theorem	moeq 1431	There is at most one set equal to a class.
⊢ ∃*x x = A
Theorem	moeq3 1432	"At most one" property of equality (split into 3 cases). (The first 2 hypotheses could be eliminated with longer proof.)
⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ ¬ (φ ∧ ψ)    ⇒   ⊢ ∃*x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))
Theorem	mosub 1433	"At most one" remains true after substitution.
⊢ ∃*xφ    ⇒   ⊢ ∃*x∃y(y = A ∧ φ)
Theorem	mo2icl 1434	Theorem for inferring "at most one".
⊢ (∀x(φ → x = A) → ∃*xφ)
Theorem	euxfr2 1435	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
⊢ A ∈ V    &   ⊢ ∃*y x = A    ⇒   ⊢ (∃!x∃y(x = A ∧ φ) ↔ ∃!yφ)
Theorem	euxfr 1436	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
⊢ A ∈ V    &   ⊢ ∃!y x = A    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (∃!xφ ↔ ∃!yψ)
Theorem	ru 1437	Russell's Paradox. Proposition 4.14 of [TakeutiZaring] p. 14. Frege's Axiom of (unrestricted) Comprehension, expressed in our notation as A ∈ V, asserted that any collection of sets A is a set i.e. belongs to the universe V of all sets. In particular, by substituting {x∣x ∉ x} for A, it asserted {x∣x ∉ x} ∈ V, meaning that the "collection of all sets which are not members of themselves" is a set. However, here we prove {x∣x ∉ x} ∉ V. This contradiction was discovered by Russell in 1901 (published in 1903), invalidating Comprehension and leading to the collapse of Frege's system. In 1908 Zermelo rectified this fatal flaw by replacing Comprehension with a weaker Subset (or Separation) Axiom ssex 1700 asserting that A is a set only when it is smaller than some other set B. However, Zermelo was then faced with a "chicken and egg" problem of how to show B is a set, leading him to introduce the set-building axioms of Null Set 0ex 1745, Pairing prex 1892, Union uniex 1947, Power Set pwex 1806, and Infinity omex 3475 to give him some starting sets to work with (all of which, before Russell's Paradox, were immediate consequences of Frege's Comprehension). In 1922 Fraenkel strengthened the Subset Axiom with our present Replacement Axiom funimaex 2716 (whose modern formalization is due to Skolem, also in 1922). Thus in a very real sense Russell's Paradox spawned the invention of ZF set theory and completely revised the foundations of mathematics! Another mainstream formalization of set theory, devised by von Neumann, Bernays, and Goedel, uses class variables rather than set variables as its primitives. The axiom system NBG in [Mendelson] p. 225 is suitable for a Metamath encoding. NBG is a conservative extension of ZF in that it proves exactly the same theorems as ZF that are expressible in the language of ZF. An advantage of NBG is that it is finitely axiomatizable - the Axiom of Replacement can be broken down into a finite set of formulas that eliminate its wff metavariable. Finite axiomatizability is required by some proof languages (although not by Metamath). There is a stronger version of NBG called Morse-Kelley (axiom system MK in [Mendelson] p. 287). Russell himself continued in a different direction, avoiding the paradox with his "theory of types." Quine extended Russell's ideas to formulate the very strong New Foundations set theory (axiom system NF of [Quine] p. 331). In NF the set of all sets is a set, contradicting ZF and NBG set theories, and it has other bizarre consequences: when sets become too huge (beyond the size of those used in standard mathematics), the Axiom of Choice ac4 3571 and Cantor's Theorem canth2 3381 are provably false! Nonetheless NF has not been shown to be inconsistent and has its advocates - who's to say which set theory is "right"? NF is finitely axiomatizable and can be encoded in Metamath using the axioms from T. Hailperin, "A set of axioms for logic," J. Symb. Logic 9:1-19 (1944).
⊢ {x∣x ∉ x} ∉ V
Theorem	vsbcint 1438	Change variable of an implicit substitution hypothesis, introducing an explicit substitution. (Contributed by Raph Levien, 10-Apr-04.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (y = A → ([y / x]φ ↔ ψ))
Theorem	sbralie 1439	Implicit to explicit substitution that swaps variables in a quantified expression.
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ ([x / y]∀x ∈ y φ ↔ ∀y ∈ x ψ)
Syntax	wsbc 1440	Extend wff notation to include the proper substitution of a class for a set. This definition "overloads" the previously defined variable substitution wsb 852 (where the first argument is a set variable rather than a class variable). We take care to ensure that this new definition is a conservative extension. Read this notation as "the proper substitution of class A for set variable x in wff φ".
wff [A / x]φ
Definition	df-sbc 1441	Define the proper substitution of a class for a set. This definition applies to proper classes but is not meaningful in that case (and does not produce the same results as Definition 6.6 of [Quine] p. 42). This definition is somewhat arbitrary - e.g., we could have used sbc6 1453 which yields a different result for proper classes. In order to allow for a possible alternate but conflicting definition in the future, we will use this definition only to prove dfsbcq 1442, which will then in turn serve as our "real" definition. Note: this definition extends or "overloads" df-sb 853 which ( via df-clab 1093) becomes a special case of it. Theorem sbab 1188 shows how proper substitution into a class variable (as opposed to a wff) could be defined. (We do not have a separate notation for it at this time.)
⊢ ([A / x]φ ↔ A ∈ {x∣φ})
Theorem	dfsbcq 1442	This theorem, which is similar to Theorem 6.7 of [Quine] p. 42, provides us a weak definition of the proper substitution of a class for a set that we will use in place of df-sbc 1441 above. We derive all our results from starting from here instead of df-sbc 1441; in particular, substitution will become undefined when A or B is a proper class. This will leave unspecified the "official" behavior for proper classes, which could be as in the sbc5 1452 assertion (always false) or as in sbc6 1453 (always true) or some more meaningful possibility in the future, that some clever person may discover, that is closer to Quine's definition. (Quine's actual definition cannot be expressed simply in our formal system.)
⊢ (A = B → ([A / x]φ ↔ [B / x]φ))
Theorem	sbceq1 1443	Equality theorem for class substitution.
⊢ (x = A → (φ ↔ [A / x]φ))
Theorem	a4sbc 1444	Specialization: if a formula is true for all sets, it is true for any class which is a set. Similar to Theorem 6.11 of [Quine] p. 44.
⊢ (A ∈ B → (∀xφ → [A / x]φ))
Theorem	hbsbcg 1445	Bound variable hypothesis builder for class substitution.
⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (A ∈ B → ([A / x]φ → ∀x[A / x]φ))
Theorem	hbsbc 1446	Bound variable hypothesis builder for class substitution. (The antecedent ensures that A is a set, which is necessary if we restrict ourselves to using only the "weak" class substitution definition dfsbcq 1442.)
⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ ((A ∈ B → [A / x]φ) → ∀x(A ∈ B → [A / x]φ))
Theorem	hbsbcv 1447	Bound variable hypothesis builder for class substitution.
⊢ A ∈ V    ⇒   ⊢ ([A / x]φ → ∀x[A / x]φ)
Theorem	sbcco 1448	A composition law for class substitution.
⊢ (A ∈ B → ([A / y][y / x]φ ↔ [A / x]φ))
Theorem	sbcco2 1449	A composition law for class substitution. Importantly, x may occur free in the class expression substituted for A.
⊢ (x = y → A = B)    ⇒   ⊢ ([x / y][B / x]φ ↔ [A / x]φ)
Theorem	sbc5g 1450	An equivalence for class substitution.
⊢ (A ∈ B → ([A / x]φ ↔ ∃x(x = A ∧ φ)))
Theorem	sbc6g 1451	An equivalence for class substitution.
⊢ (A ∈ B → ([A / x]φ ↔ ∀x(x = A → φ)))
Theorem	sbc5 1452	An equivalence for class substitution.
⊢ A ∈ V    ⇒   ⊢ ([A / x]φ ↔ ∃x(x = A ∧ φ))
Theorem	sbc6 1453	An equivalence for class substitution.
⊢ A ∈ V    ⇒   ⊢ ([A / x]φ ↔ ∀x(x = A → φ))
Theorem	sbc2or 1454	The disjunction of two equivalences for class substitution does not require a class existence hypothesis.
⊢ (([A / x]φ ↔ ∃x(x = A ∧ φ)) ∨ ([A / x]φ ↔ ∀x(x = A → φ)))
Theorem	sbcie 1455	Conversion of implicit substitution to explicit class substitution.
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ([A / x]φ ↔ ψ)
Theorem	elrabsf 1456	Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf 1421 has implicit substitution). The hypothesis specifies that x must not be a free variable in B.
⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (A ∈ {x ∈ B∣φ} ↔ (A ∈ B ∧ [A / x]φ))
Theorem	elabs2 1457	Membership in a class abstraction, expressed in terms of class substitution. Theorem 6.13 of [Quine] p. 44.
⊢ (A ∈ {x∣φ} ↔ (A ∈ V ∧ [A / x]φ))
Theorem	elabs 1458	Membership in a class abstraction, expressed in terms of class substitution. Conveniently, this theorem has no distinct variable restrictions. Except for the existence hypothesis, this theorem is "almost" like df-sbc 1441 but was proved using only dfsbcq 1442 as its starting point (making no other reference to df-sbc 1441). We prefer not to make direct reference to df-sbc 1441 since its behavior at proper classes is at odds with Quine, whereas dfsbcq 1442 is not. (Quine's class substitution cannot be expressed in closed form.) This theorem serves as a Quine-compatible substitute for df-sbc 1441.
⊢ A ∈ V    ⇒   ⊢ (A ∈ {x∣φ} ↔ [A / x]φ)
Theorem	sbcn 1459	Move negation in and out of class substitution.
⊢ (A ∈ B → ([A / x] ¬ φ ↔ ¬ [A / x]φ))
Theorem	sbcim 1460	Distribution of class substitution over implication.
⊢ (A ∈ B → ([A / x](φ → ψ) ↔ ([A / x]φ → [A / x]ψ)))
Theorem	sbcan 1461	Distribution of class substitution over conjunction.
⊢ (A ∈ B → ([A / x](φ ∧ ψ) ↔ ([A / x]φ ∧ [A / x]ψ)))
Theorem	sbcor 1462	Distribution of class substitution over disjunction.
⊢ (A ∈ B → ([A / x](φ ∨ ψ) ↔ ([A / x]φ ∨ [A / x]ψ)))
Theorem	sbcbi 1463	Distribution of class substitution over biconditional. (Contributed by Raph Levien, 10-Apr-04.)
⊢ (A ∈ B → ([A / x](φ ↔ ψ) ↔ ([A / x]φ ↔ [A / x]ψ)))
Theorem	sbcal 1464	Move universal quantifier in and out of class substitution.
⊢ (A ∈ B → ([A / y]∀xφ ↔ ∀x[A / y]φ))
Theorem	sbcex 1465	Move existential quantifier in and out of class substitution.
⊢ (A ∈ B → ([A / y]∃xφ ↔ ∃x[A / y]φ))
Theorem	sbcel1 1466	Class substitution into a membership relation.
⊢ (A ∈ C → ([A / x]x ∈ B ↔ A ∈ B))
Theorem	sbcel2 1467	Class substitution into a membership relation.
⊢ (B ∈ C → ([B / x]A ∈ x ↔ A ∈ B))
Theorem	bisbcdv 1468	Formula-building deduction rule for class substitution.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ ((A ∈ B ∧ φ) → ([A / x]ψ ↔ [A / x]χ))
Theorem	sbcgf 1469	Substitution for a variable not free in a wff does not affect it.
⊢ (φ → ∀xφ)    ⇒   ⊢ (A ∈ B → ([A / x]φ ↔ φ))
Theorem	sbc19.21g 1470	Substitution for a variable not free in antecedent affects only the consequent.
⊢ (φ → ∀xφ)    ⇒   ⊢ (A ∈ B → ([A / x](φ → ψ) ↔ (φ → [A / x]ψ)))
Theorem	rax4 1471	Restricted quantifier version of Axiom 4 of [Mendelson] p. 59. This is an axiom of a predicate calculus for a restricted domain. Compare the unrestricted stdpc4 869.
⊢ (B ∈ A → (∀x ∈ A φ → [B / x]φ))
Theorem	rax5 1472	Restricted quantifier version of Axiom 5 of [Mendelson] p. 59. This is an axiom of a predicate calculus for a restricted domain. Compare the unrestricted stdpc5 739.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x ∈ A (φ → ψ) → (φ → ∀x ∈ A ψ))
Theorem	axrep 1473	Axiom of Replacement expressed more compactly, with fewest number of different variables.
⊢ ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ)))
Theorem	axrep2 1474	Axiom of Replacement slightly strengthened from axrep 1473; w may occur free in φ.
⊢ ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ w ∧ ∀yφ)))
Theorem	zfrep2 1475	A more traditional version of the Axiom of Replacement.
⊢ (φ → ∀zφ)    ⇒   ⊢ (∀x∃z∀y(φ → y = z) → ∃z∀y(y ∈ z ↔ ∃x(x ∈ w ∧ φ)))
Theorem	zfrep3 1476	Axiom of Replacement (similar to Axiom Rep of [BellMachover] p. 463). The antecedent tells us φ is analogous to a "function" from x to y (although it is not really a function since it is a wff and not a class). In the consequent we postulate the existence of a set z that corresponds to the "image" of φ restricted to some other set w. The hypothesis says z must not be free in φ.
⊢ (φ → ∀zφ)    ⇒   ⊢ (∀x(x ∈ w → ∃z∀y(φ → y = z)) → ∃z∀y(y ∈ z ↔ ∃x(x ∈ w ∧ φ)))
Theorem	zfrepclf 1477	An inference rule based on the Axiom of Replacement. Typically, φ defines a function from x to y.
⊢ (w ∈ A → ∀x w ∈ A)    &   ⊢ A ∈ V    &   ⊢ (x ∈ A → ∃z∀y(φ → y = z))    ⇒   ⊢ ∃z∀y(y ∈ z ↔ ∃x(x ∈ A ∧ φ))
Theorem	zfrep3cl 1478	An inference rule based on the Axiom of Replacement. Typically, φ defines a function from x to y.
⊢ A ∈ V    &   ⊢ (x ∈ A → ∃z∀y(φ → y = z))    ⇒   ⊢ ∃z∀y(y ∈ z ↔ ∃x(x ∈ A ∧ φ))
Theorem	zfrep4 1479	A version of Replacement using class abstractions.
⊢ {x∣φ} ∈ V    &   ⊢ (φ → ∃z∀y(ψ → y = z))    ⇒   ⊢ {y∣∃x(φ ∧ ψ)} ∈ V
Theorem	zfaus 1480	Separation Scheme, which is an axiom scheme of Zermelo's original theory. Scheme Sep of [BellMachover] p. 463. In some textbooks this is given as a separate axiom; here we show it is redundant if we assume ax-rep 1075. The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with x ∈ A) so that it asserts the existence of a collection only if it is smaller than some other collection A that already exists. This prevents Russell's paradox ru 1437. In some texts this scheme is called "Aussonderung" or the Subset Axiom. In typical applications the variable x is free in the wff φ.
⊢ A ∈ V    ⇒   ⊢ ∃y∀x(x ∈ y ↔ (x ∈ A ∧ φ))
Theorem	bm1.3ii 1481	Convert implication to equivalence using Aussonderung. Similar to Theorem 1.3ii of [BellMachover] p. 463.
⊢ ∃x∀y(φ → y ∈ x)    ⇒   ⊢ ∃x∀y(y ∈ x ↔ φ)
Theorem	nalset 1482	No set contains all sets. Theorem 41 of [Suppes] p. 30.
⊢ ¬ ∃x∀y y ∈ x
Theorem	nvelv 1483	The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity.
⊢ ¬ V ∈ V
Syntax	cdif 1484	Extend class notation to include class difference (read: "A minus B").
class (A ∖ B)
Syntax	cun 1485	Extend class notation to include union of two classes (read: "A union B").
class (A ∪ B)
Syntax	cin 1486	Extend class notation to include the intersection of two classes (read: "A intersect B").
class (A ∩ B)
Syntax	wss 1487	Extend wff notation to include the subclass relation. This is read "A is a subclass of B" or "B includes A." When A exists as a set, it is also read "A is a subset of B."
wff A ⊆ B
Syntax	wpss 1488	Extend wff notation with proper subclass relation.
wff A ⊂ B
Definition	df-dif 1489	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. Several notations are used in the literature; we chose the ∖ convention used in Definition 5.3 of [Eisenberg] p. 67 instead of the more common minus sign to reserve the latter for later use in, e.g., arithmetic.
⊢ (A ∖ B) = {x∣(x ∈ A ∧ ¬ x ∈ B)}
Definition	df-un 1490	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 1668. For union defined in terms of intersection, see dfun3 1671.
⊢ (A ∪ B) = {x∣(x ∈ A ∨ x ∈ B)}
Definition	df-in 1491	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 1669 and dfin4 1673. For intersection defined in terms of union, see dfin3 1672.
⊢ (A ∩ B) = {x∣(x ∈ A ∧ x ∈ B)}
Definition	df-ss 1492	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 1497. Other possible definitions are given by dfss3 1498, dfss4 1667, sspss 1569, ssequn1 1628, ssequn2 1631, sseqin2 1656, and ssdif0 1748.
⊢ (A ⊆ B ↔ (A ∩ B) = A)
Theorem	dfss 1493	A frequently-used variant of subclass definition df-ss 1492.
⊢ (A ⊆ B ↔ A = (A ∩ B))
Definition	df-pss 1494	Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. Other possible definitions are given by dfpss2 1557 and dfpss3 1558.
⊢ (A ⊂ B ↔ (A ⊆ B ∧ A ≠ B))
Theorem	dfdif2 1495	Alternate definition of class difference.
⊢ (A ∖ B) = {x ∈ A∣ ¬ x ∈ B}
Theorem	eldif 1496	Expansion of membership in a class difference.
⊢ (A ∈ (B ∖ C) ↔ (A ∈ B ∧ ¬ A ∈ C))
Theorem	dfss2 1497	Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17.
⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
Theorem	dfss3 1498	Alternate definition of subclass relationship.
⊢ (A ⊆ B ↔ ∀x ∈ A x ∈ B)
Theorem	dfss2f 1499	Equivalence for subclass relation requiring only that x not be free in A and B (but not necessarily absent from them).
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
Theorem	dfss3f 1500	Equivalence for subclass relation requiring only that x not be free in A and B (but not necessarily absent from them).
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (A ⊆ B ↔ ∀x ∈ A x ∈ B)