P. 45 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4401-4500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elsuc2 4401	Membership in a successor. (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))
Theorem	nfsuc 4402	Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 suc 𝐴
Theorem	elelsuc 4403	Membership in a successor. (Contributed by NM, 20-Jun-1998.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵)
Theorem	sucel 4404*	Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)))
Theorem	suc0 4405	The successor of the empty set. (Contributed by NM, 1-Feb-2005.)
⊢ suc ∅ = {∅}
Theorem	sucprc 4406	A proper class is its own successor. (Contributed by NM, 3-Apr-1995.)
⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
Theorem	unisuc 4407	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴)
Theorem	unisucg 4408	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by Jim Kingdon, 18-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴))
Theorem	sssucid 4409	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)
⊢ 𝐴 ⊆ suc 𝐴
Theorem	sucidg 4410	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)
Theorem	sucid 4411	A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ suc 𝐴
Theorem	nsuceq0g 4412	No successor is empty. (Contributed by Jim Kingdon, 14-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ≠ ∅)
Theorem	eqelsuc 4413	A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵)
Theorem	iunsuc 4414*	Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ suc 𝐴𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶)
Theorem	suctr 4415	The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.)
⊢ (Tr 𝐴 → Tr suc 𝐴)
Theorem	trsuc 4416	A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
Theorem	trsucss 4417	A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.)
⊢ (Tr 𝐴 → (𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	sucssel 4418	A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.)
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
Theorem	orduniss 4419	An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴)
Theorem	onordi 4420	An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ Ord 𝐴
Theorem	ontrci 4421	An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ Tr 𝐴
Theorem	oneli 4422	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ On)
Theorem	onelssi 4423	A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)
Theorem	onelini 4424	An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴))
Theorem	oneluni 4425	An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴)
Theorem	onunisuci 4426	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ ∪ suc 𝐴 = 𝐴
2.4  IZF Set Theory - add the Axiom of Union
2.4.1  Introduce the Axiom of Union
Axiom	ax-un 4427*	Axiom of Union. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set 𝑦 exists that includes the union of a given set 𝑥 i.e. the collection of all members of the members of 𝑥. The variant axun2 4429 states that the union itself exists. A version with the standard abbreviation for union is uniex2 4430. A version using class notation is uniex 4431. This is Axiom 3 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4119), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 266). The union of a class df-uni 3806 should not be confused with the union of two classes df-un 3131. Their relationship is shown in unipr 3819. (Contributed by NM, 23-Dec-1993.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfun 4428*	Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axun2 4429*	A variant of the Axiom of Union ax-un 4427. For any set 𝑥, there exists a set 𝑦 whose members are exactly the members of the members of 𝑥 i.e. the union of 𝑥. Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
Theorem	uniex2 4430*	The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦 𝑦 = ∪ 𝑥
Theorem	uniex 4431	The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 2741), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ 𝐴 ∈ V
Theorem	vuniex 4432	The union of a setvar is a set. (Contributed by BJ, 3-May-2021.)
⊢ ∪ 𝑥 ∈ V
Theorem	uniexg 4433	The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.)
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
Theorem	uniexd 4434	Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ V)
Theorem	unex 4435	The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ V
Theorem	unexb 4436	Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
Theorem	unexg 4437	A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	tpexg 4438	An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {𝐴, 𝐵, 𝐶} ∈ V)
Theorem	unisn3 4439*	Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.)
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴} = 𝐴)
Theorem	abnexg 4440*	Sufficient condition for a class abstraction to be a proper class. The class 𝐹 can be thought of as an expression in 𝑥 and the abstraction appearing in the statement as the class of values 𝐹 as 𝑥 varies through 𝐴. Assuming the antecedents, if that class is a set, then so is the "domain" 𝐴. The converse holds without antecedent, see abrexexg 6109. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 4442 and pwnex 4443 respectively, proved from abnex 4441, which is a consequence of abnexg 4440 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.)
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V))
Theorem	abnex 4441*	Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 4442 and pwnex 4443. See the comment of abnexg 4440. (Contributed by BJ, 2-May-2021.)
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V)
Theorem	snnex 4442*	The class of all singletons is a proper class. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.)
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V
Theorem	pwnex 4443*	The class of all power sets is a proper class. See also snnex 4442. (Contributed by BJ, 2-May-2021.)
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V
Theorem	opeluu 4444	Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → (𝐴 ∈ ∪ ∪ 𝐶 ∧ 𝐵 ∈ ∪ ∪ 𝐶))
Theorem	uniuni 4445*	Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.)
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)}
Theorem	eusv1 4446*	Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.)
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ ∃𝑦∀𝑥 𝑦 = 𝐴)
Theorem	eusvnf 4447*	Even if 𝑥 is free in 𝐴, it is effectively bound when 𝐴(𝑥) is single-valued. (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴)
Theorem	eusvnfb 4448*	Two ways to say that 𝐴(𝑥) is a set expression that does not depend on 𝑥. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V))
Theorem	eusv2i 4449*	Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 18-Nov-2016.)
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴)
Theorem	eusv2nf 4450*	Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴)
Theorem	eusv2 4451*	Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ ∃!𝑦∀𝑥 𝑦 = 𝐴)
Theorem	reusv1 4452*	Two ways to express single-valuedness of a class expression 𝐶(𝑦). (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ (∃𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
Theorem	reusv3i 4453*	Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷))
Theorem	reusv3 4454*	Two ways to express single-valuedness of a class expression 𝐶(𝑦). See reusv1 4452 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    ⇒   ⊢ (∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝐶 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
Theorem	alxfr 4455*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 18-Feb-2007.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((∀𝑦 𝐴 ∈ 𝐵 ∧ ∀𝑥∃𝑦 𝑥 = 𝐴) → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	ralxfrd 4456*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))
Theorem	rexxfrd 4457*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by FL, 10-Apr-2007.) (Revised by Mario Carneiro, 15-Aug-2014.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒))
Theorem	ralxfr2d 4458*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))
Theorem	rexxfr2d 4459*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒))
Theorem	ralxfr 4460*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.)
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓)
Theorem	ralxfrALT 4461*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. This proof does not use ralxfrd 4456. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓)
Theorem	rexxfr 4462*	Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.)
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐶 𝜓)
Theorem	rabxfrd 4463*	Class builder membership after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the class expression 𝜒. (Contributed by NM, 16-Jan-2012.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐴 ∈ 𝐷)    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐷) → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜓} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜒}))
Theorem	rabxfr 4464*	Class builder membership after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the class expression 𝜑. (Contributed by NM, 10-Jun-2005.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ (𝑦 ∈ 𝐷 → 𝐴 ∈ 𝐷)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶)    ⇒   ⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜑} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜓}))
Theorem	reuhypd 4465*	A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 16-Jan-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)
Theorem	reuhyp 4466*	A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 15-Nov-2004.)
⊢ (𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶)    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵))    ⇒   ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)
Theorem	uniexb 4467	The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.)
⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V)
Theorem	pwexb 4468	The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003.)
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
Theorem	elpwpwel 4469	A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.)
⊢ (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵)
Theorem	univ 4470	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.)
⊢ ∪ V = V
Theorem	eldifpw 4471	Membership in a power class difference. (Contributed by NM, 25-Mar-2007.)
⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵))
Theorem	op1stb 4472	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ⟨𝐴, 𝐵⟩ = 𝐴
Theorem	op1stbg 4473	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by Jim Kingdon, 17-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ ∩ ⟨𝐴, 𝐵⟩ = 𝐴)
Theorem	iunpw 4474*	An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥)
Theorem	ifelpwung 4475	Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵))
Theorem	ifelpwund 4476	Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵))
Theorem	ifelpwun 4477	Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵)
Theorem	ifexd 4478	Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ V)
2.4.2  Ordinals (continued)
Theorem	ordon 4479	The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.)
⊢ Ord On
Theorem	ssorduni 4480	The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴)
Theorem	ssonuni 4481	The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. (Contributed by NM, 1-Nov-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊆ On → ∪ 𝐴 ∈ On))
Theorem	ssonunii 4482	The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ⊆ On → ∪ 𝐴 ∈ On)
Theorem	onun2 4483	The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On)
Theorem	onun2i 4484	The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) (Constructive proof by Jim Kingdon, 25-Jul-2019.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ On
Theorem	ordsson 4485	Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.)
⊢ (Ord 𝐴 → 𝐴 ⊆ On)
Theorem	onss 4486	An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
Theorem	onuni 4487	The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On)
Theorem	orduni 4488	The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.)
⊢ (Ord 𝐴 → Ord ∪ 𝐴)
Theorem	bm2.5ii 4489*	Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ⊆ On → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	sucexb 4490	A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.)
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
Theorem	sucexg 4491	The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V)
Theorem	sucex 4492	The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ suc 𝐴 ∈ V
Theorem	ordsucim 4493	The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 8-Nov-2018.)
⊢ (Ord 𝐴 → Ord suc 𝐴)
Theorem	suceloni 4494	The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)
Theorem	ordsucg 4495	The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 20-Nov-2018.)
⊢ (𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴))
Theorem	sucelon 4496	The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.)
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)
Theorem	ordsucss 4497	The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.)
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
Theorem	ordelsuc 4498	A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 29-Nov-2003.)
⊢ ((𝐴 ∈ 𝐶 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵))
Theorem	onsucssi 4499	A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 16-Sep-1995.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵)
Theorem	onsucmin 4500*	The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.)
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥})