P. 54 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5301-5400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	intv 5301	The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.)
⊢ ∩ V = ∅
2.3  ZF Set Theory - add the Axiom of Power Sets
2.3.1  Introduce the Axiom of Power Sets
Axiom	ax-pow 5302*	Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory. It states that a set 𝑦 exists that includes the power set of a given set 𝑥 i.e. contains every subset of 𝑥. The variant axpow2 5304 uses explicit subset notation. A version using class notation is pwex 5317. (Contributed by NM, 21-Jun-1993.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfpow 5303*	Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpow2 5304*	A variant of the Axiom of Power Sets ax-pow 5302 using subset notation. Problem in [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)
Theorem	axpow3 5305*	A variant of the Axiom of Power Sets ax-pow 5302. For any set 𝑥, there exists a set 𝑦 whose members are exactly the subsets of 𝑥 i.e. the power set of 𝑥. Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 ↔ 𝑧 ∈ 𝑦)
Theorem	elALT2 5306*	Alternate proof of el 5385 using ax-9 2124 and ax-pow 5302 instead of ax-pr 5370. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	dtruALT2 5307*	Alternate proof of dtru 5384 using ax-pow 5302 instead of ax-pr 5370. See dtruALT 5325 for another proof using ax-pow 5302 instead of ax-pr 5370. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2377. (Revised by BJ, 31-May-2019.) Avoid ax-12 2185. (Revised by Rohan Ridenour, 9-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	dtrucor 5308*	Corollary of dtru 5384. This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid, as shown by dtrucor2 5309. (Contributed by NM, 27-Jun-2002.)
⊢ 𝑥 = 𝑦    ⇒   ⊢ 𝑥 ≠ 𝑦
Theorem	dtrucor2 5309	The theorem form of the deduction dtrucor 5308 leads to a contradiction, as mentioned in the "Wrong!" example at mmdeduction.html#bad 5308. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by NM, 20-Oct-2007.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦)    ⇒   ⊢ (𝜑 ∧ ¬ 𝜑)
Theorem	dvdemo1 5310*	Demonstration of a theorem that requires the setvar variables 𝑥 and 𝑦 to be disjoint (but without any other disjointness conditions, and in particular, none on 𝑧). That theorem bundles the theorems (⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) with 𝑥, 𝑦, 𝑧 disjoint), often called its "principal instance", and the two "degenerate instances" (⊢ ∃𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥) with 𝑥, 𝑦 disjoint) and (⊢ ∃𝑥(𝑥 = 𝑦 → 𝑦 ∈ 𝑥) with 𝑥, 𝑦 disjoint). Compare with dvdemo2 5311, which has the same principal instance and one common degenerate instance but crucially differs in the other degenerate instance. See https://us.metamath.org/mpeuni/mmset.html#distinct 5311 for details on the "disjoint variable" mechanism. (The verb "bundle" to express this phenomenon was introduced by Raph Levien.) Note that dvdemo1 5310 is partially bundled, in that the pairs of setvar variables 𝑥, 𝑧 and 𝑦, 𝑧 need not be disjoint, and in spite of that, its proof does not require ax-11 2163 nor ax-13 2377. (Contributed by NM, 1-Dec-2006.) (Revised by BJ, 13-Jan-2024.)
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)
Theorem	dvdemo2 5311*	Demonstration of a theorem that requires the setvar variables 𝑥 and 𝑧 to be disjoint (but without any other disjointness conditions, and in particular, none on 𝑦). That theorem bundles the theorems (⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) with 𝑥, 𝑦, 𝑧 disjoint), often called its "principal instance", and the two "degenerate instances" (⊢ ∃𝑥(𝑥 = 𝑥 → 𝑧 ∈ 𝑥) with 𝑥, 𝑧 disjoint) and (⊢ ∃𝑥(𝑥 = 𝑧 → 𝑧 ∈ 𝑥) with 𝑥, 𝑧 disjoint). Compare with dvdemo1 5310, which has the same principal instance and one common degenerate instance but crucially differs in the other degenerate instance. See https://us.metamath.org/mpeuni/mmset.html#distinct 5310 for details on the "disjoint variable" mechanism. Note that dvdemo2 5311 is partially bundled, in that the pairs of setvar variables 𝑥, 𝑦 and 𝑦, 𝑧 need not be disjoint, and in spite of that, its proof does not require any of the auxiliary axioms ax-10 2147, ax-11 2163, ax-12 2185, ax-13 2377. (Contributed by NM, 1-Dec-2006.) Avoid ax-13 2377. (Revised by BJ, 13-Jan-2024.)
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)
Theorem	nfnid 5312	A setvar variable is not free from itself. This theorem is not true in a one-element domain, as illustrated by the use of dtruALT2 5307 in its proof. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ ¬ Ⅎ𝑥𝑥
Theorem	nfcvb 5313	The "distinctor" expression ¬ ∀𝑥𝑥 = 𝑦, stating that 𝑥 and 𝑦 are not the same variable, can be written in terms of Ⅎ in the obvious way. This theorem is not true in a one-element domain, because then Ⅎ𝑥𝑦 and ∀𝑥𝑥 = 𝑦 will both be true. (Contributed by Mario Carneiro, 8-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2377. (New usage is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	vpwex 5314	Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 5315 from vpwex 5314. (Revised by BJ, 10-Aug-2022.)
⊢ 𝒫 𝑥 ∈ V
Theorem	pwexg 5315	Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
Theorem	pwexd 5316	Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
Theorem	pwex 5317	Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝒫 𝐴 ∈ V
Theorem	pwel 5318	Quantitative version of pwexg 5315: the powerset of an element of a class is an element of the double powerclass of the union of that class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) Remove use of ax-nul 5241 and ax-pr 5370 and shorten proof. (Revised by BJ, 13-Apr-2024.)
⊢ (𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 ∪ 𝐵)
Theorem	abssexg 5319*	Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V)
Theorem	snexALT 5320	Alternate proof of snex 5376 using Power Set (ax-pow 5302) instead of Pairing (ax-pr 5370). Unlike in the proof of zfpair 5358, Replacement (ax-rep 5212) is not needed. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴} ∈ V
Theorem	p0ex 5321	The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5322. (Contributed by NM, 23-Dec-1993.)
⊢ {∅} ∈ V
Theorem	p0exALT 5322	Alternate proof of p0ex 5321 which is quite different and longer if snexALT 5320 is expanded. (Contributed by NM, 23-Dec-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {∅} ∈ V
Theorem	pp0ex 5323	The power set of the power set of the empty set (the ordinal 2) is a set. (Contributed by NM, 24-Jun-1993.)
⊢ {∅, {∅}} ∈ V
Theorem	ord3ex 5324	The ordinal number 3 is a set, proved without the Axiom of Union ax-un 7682. (Contributed by NM, 2-May-2009.)
⊢ {∅, {∅}, {∅, {∅}}} ∈ V
Theorem	dtruALT 5325*	Alternate proof of dtru 5384 which requires more axioms but is shorter and may be easier to understand. Like dtruALT2 5307, it uses ax-pow 5302 rather than ax-pr 5370. Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that 𝑥 and 𝑦 be distinct. Specifically, Theorem spcev 3549 requires that 𝑥 must not occur in the subexpression ¬ 𝑦 = {∅} in step 4 nor in the subexpression ¬ 𝑦 = ∅ in step 9. The proof verifier will require that 𝑥 and 𝑦 be in a distinct variable group to ensure this. You can check this by deleting the $d statement in set.mm and rerunning the verifier, which will print a detailed explanation of the distinct variable violation. (Contributed by NM, 15-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	axc16b 5326*	This theorem shows that Axiom ax-c16 39352 is redundant in the presence of Theorem dtruALT2 5307, which states simply that at least two things exist. This justifies the remark at mmzfcnd.html#twoness 5307 (which links to this theorem). (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 7-Nov-2006.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	eunex 5327	Existential uniqueness implies there is a value for which the wff argument is false. (Contributed by NM, 24-Oct-2010.) (Proof shortened by BJ, 2-Jan-2023.)
⊢ (∃!𝑥𝜑 → ∃𝑥 ¬ 𝜑)
Theorem	eusv1 5328*	Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.)
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ ∃𝑦∀𝑥 𝑦 = 𝐴)
Theorem	eusvnf 5329*	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 5330*	Two ways to say that 𝐴(𝑥) is a set expression that does not depend on 𝑥. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V))
Theorem	eusv2i 5331*	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 5332*	Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴)
Theorem	eusv2 5333*	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 5334*	Two ways to express single-valuedness of a class expression 𝐶(𝑦). (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.)
⊢ (∃𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
Theorem	reusv2lem1 5335*	Lemma for reusv2 5340. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ (𝐴 ≠ ∅ → (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	reusv2lem2 5336*	Lemma for reusv2 5340. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.)
⊢ (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵)
Theorem	reusv2lem3 5337*	Lemma for reusv2 5340. (Contributed by NM, 14-Dec-2012.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ (∀𝑦 ∈ 𝐴 𝐵 ∈ V → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	reusv2lem4 5338*	Lemma for reusv2 5340. (Contributed by NM, 13-Dec-2012.)
⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝐶))
Theorem	reusv2lem5 5339*	Lemma for reusv2 5340. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ ((∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 = 𝐶))
Theorem	reusv2 5340*	Two ways to express single-valuedness of a class expression 𝐶(𝑦) that is constant for those 𝑦 ∈ 𝐵 such that 𝜑. The first antecedent ensures that the constant value belongs to the existential uniqueness domain 𝐴, and the second ensures that 𝐶(𝑦) is evaluated for at least one 𝑦. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
Theorem	reusv3i 5341*	Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷))
Theorem	reusv3 5342*	Two ways to express single-valuedness of a class expression 𝐶(𝑦). See reusv1 5334 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    ⇒   ⊢ (∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝐶 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
Theorem	eusv4 5343*	Two ways to express single-valuedness of a class expression 𝐵(𝑦). (Contributed by NM, 27-Oct-2010.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)
Theorem	alxfr 5344*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 18-Feb-2007.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((∀𝑦 𝐴 ∈ 𝐵 ∧ ∀𝑥∃𝑦 𝑥 = 𝐴) → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	ralxfrd 5345*	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.) (Proof shortened by JJ, 7-Aug-2021.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))
Theorem	rexxfrd 5346*	Transfer existential 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 5347*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))
Theorem	rexxfr2d 5348*	Transfer existential 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	ralxfrd2 5349*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of ralxfrd 5345. (Contributed by Alexander van der Vekens, 25-Apr-2018.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))
Theorem	rexxfrd2 5350*	Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of rexxfrd 5346. (Contributed by Alexander van der Vekens, 25-Apr-2018.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒))
Theorem	ralxfr 5351*	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 5352*	Alternate proof of ralxfr 5351 which does not use ralxfrd 5345. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓)
Theorem	rexxfr 5353*	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 5354*	Membership in a restricted class abstraction after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the formula defining the class abstraction. (Contributed by NM, 16-Jan-2012.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐴 ∈ 𝐷)    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐷) → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜓} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜒}))
Theorem	rabxfr 5355*	Membership in a restricted class abstraction after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the formula defining the class abstraction. (Contributed by NM, 10-Jun-2005.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ (𝑦 ∈ 𝐷 → 𝐴 ∈ 𝐷)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶)    ⇒   ⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜑} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜓}))
Theorem	reuhypd 5356*	A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd 7351. (Contributed by NM, 16-Jan-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)
Theorem	reuhyp 5357*	A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr1 3699. (Contributed by NM, 15-Nov-2004.)
⊢ (𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶)    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵))    ⇒   ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)
Theorem	zfpair 5358	The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of [TakeutiZaring] p. 15. In some textbooks this is stated as a separate axiom; here we show it is redundant since it can be derived from the other axioms. This theorem should not be referenced by any proof other than axprALT 5359. Instead, use zfpair2 5371 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	axprALT 5359*	Alternate proof of axpr 5364. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
2.3.2  Derive the Axiom of Pairing
Theorem	axprlem1 5360*	Lemma for axpr 5364. There exists a set to which all empty sets belong. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) (Proof shortened by Matthew House, 6-Apr-2026.)
⊢ ∃𝑥∀𝑦(∀𝑧 ¬ 𝑧 ∈ 𝑦 → 𝑦 ∈ 𝑥)
Theorem	axprlem2 5361*	Lemma for axpr 5364. There exists a set to which all sets whose only members are empty sets belong. (Contributed by Rohan Ridenour, 9-Aug-2023.) (Revised by BJ, 13-Aug-2023.)
⊢ ∃𝑥∀𝑦(∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥)
Theorem	axprlem3 5362*	Lemma for axpr 5364. Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof shortened by Matthew House, 18-Sep-2025.)
⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Theorem	axprlem4 5363*	Lemma for axpr 5364. If an existing set of empty sets corresponds to one element of the pair, then the element is included in any superset of the set whose existence is asserted by the axiom of replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) (Revised by Matthew House, 18-Sep-2025.)
⊢ ∃𝑠∀𝑛𝜑    &   ⊢ (𝜑 → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))    &   ⊢ (∀𝑛𝜑 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑣))    ⇒   ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (𝑤 = 𝑣 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
Theorem	axpr 5364*	Unabbreviated version of the Axiom of Pairing of ZF set theory, derived as a theorem from the other axioms. This theorem should not be referenced by any proof. Instead, use ax-pr 5370 below so that the uses of the Axiom of Pairing can be more easily identified. For a shorter proof using ax-ext 2709, see axprALT 5359. (Contributed by NM, 14-Nov-2006.) Remove dependency on ax-ext 2709. (Revised by Rohan Ridenour, 10-Aug-2023.) (Proof shortened by BJ, 13-Aug-2023.) (Proof shortened by Matthew House, 18-Sep-2025.) Use ax-pr 5370 instead. (New usage is discouraged.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Theorem	axprlem1OLD 5365*	Obsolete version of axprlem1 5360 as of 6-Apr-2026. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(∀𝑧 ¬ 𝑧 ∈ 𝑦 → 𝑦 ∈ 𝑥)
Theorem	axprlem3OLD 5366*	Obsolete version of axprlem3 5362 as of 18-Sep-2025. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Theorem	axprlem4OLD 5367*	Obsolete version of axprlem4 5363 as of 18-Sep-2025. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Theorem	axprlem5OLD 5368*	Obsolete version of axprlem4 5363 as of 18-Sep-2025. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Theorem	axprOLD 5369*	Obsolete version of axpr 5364 as of 18-Sep-2025. (Contributed by NM, 14-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Axiom	ax-pr 5370*	The Axiom of Pairing of ZF set theory. It was derived as Theorem axpr 5364 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14-Nov-2006.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Theorem	zfpair2 5371	Derive the abbreviated version of the Axiom of Pairing from ax-pr 5370. See zfpair 5358 for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	vsnex 5372	A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.)
⊢ {𝑥} ∈ V
Theorem	axprglem 5373*	Lemma for axprg 5374. (Contributed by GG, 11-Mar-2026.)
⊢ (𝑥 = 𝐴 → ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧))
Theorem	axprg 5374*	Derive The Axiom of Pairing with class variables. (Contributed by GG, 6-Mar-2026.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
Theorem	prex 5375	The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 4712), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5241 and shorten proof. (Revised by GG, 6-Mar-2026.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	snex 5376	A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation and Pairing. See also snexALT 5320. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Avoid ax-nul 5241 and shorten proof. (Revised by GG, 6-Mar-2026.)
⊢ {𝐴} ∈ V
Theorem	snexg 5377	A singleton built on a set is a set. Special case of snex 5376 which is intuitionistically valid. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Extract from snex 5376 and shorten proof. (Revised by BJ, 15-Jan-2025.) (Proof shortened by GG, 6-Mar-2026.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	snexgALT 5378	Alternate proof of snexg 5377 based on vsnex 5372, which uses an instance of ax-sep 5231. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Extract from snex 5376 and shorten proof. (Revised by BJ, 15-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	snexOLD 5379	Obsolete version of snex 5376 as of 6-Mar-2026. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴} ∈ V
Theorem	prexOLD 5380	Obsolete version of prex 5375 as of 6-Mar-2026. (Contributed by NM, 15-Jul-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	exel 5381*	There exist two sets, one a member of the other. This theorem looks similar to el 5385, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1811, ax-6 1969, and ax-pr 5370. This theorem does not exclude that these two sets could actually be one single set containing itself. That two different sets exist is proved by exexneq 5382. (Contributed by SN, 23-Dec-2024.)
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦
Theorem	exexneq 5382*	There exist two different sets. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2377. (Revised by BJ, 31-May-2019.) Avoid ax-8 2116. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2185. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5370 instead of ax-pow 5302. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5384. (Revised by BJ, 2-Jan-2025.)
⊢ ∃𝑥∃𝑦 ¬ 𝑥 = 𝑦
Theorem	exneq 5383*	Given any set (the "𝑦 " in the statement), there exists a set not equal to it. The same statement without disjoint variable condition is false, since we do not have ∃𝑥¬ 𝑥 = 𝑥. This theorem is proved directly from set theory axioms (no class definitions) and does not depend on ax-ext 2709, ax-sep 5231, or ax-pow 5302 nor auxiliary logical axiom schemes ax-10 2147 to ax-13 2377. See dtruALT 5325 for a shorter proof using more axioms, and dtruALT2 5307 for a proof using ax-pow 5302 instead of ax-pr 5370. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2377. (Revised by BJ, 31-May-2019.) Avoid ax-8 2116. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2185. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5370 instead of ax-pow 5302. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5384. (Revised by BJ, 2-Jan-2025.)
⊢ ∃𝑥 ¬ 𝑥 = 𝑦
Theorem	dtru 5384*	Given any set (the "𝑦 " in the statement), not all sets are equal to it. The same statement without disjoint variable condition is false since it contradicts stdpc6 2030. The same comments and revision history concerning axiom usage as in exneq 5383 apply. See dtruALT 5325 and dtruALT2 5307 for alternate proofs avoiding ax-pr 5370. (Contributed by NM, 7-Nov-2006.) Extract exneq 5383 as an intermediate result. (Revised by BJ, 2-Jan-2025.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	el 5385*	Any set is an element of some other set. See elALT 5389 for a shorter proof using more axioms, and see elALT2 5306 for a proof that uses ax-9 2124 and ax-pow 5302 instead of ax-pr 5370. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Use ax-pr 5370 instead of ax-9 2124 and ax-pow 5302. (Revised by BTernaryTau, 2-Dec-2024.) (Proof shortened by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	elOLD 5386*	Obsolete version of el 5385 as of 6-Apr-2026. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	sels 5387*	If a class is a set, then it is a member of a set. (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5389. (Revised by BJ, 3-Apr-2019.) Avoid ax-sep 5231, ax-nul 5241, ax-pow 5302. (Revised by BTernaryTau, 15-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	selsALT 5388*	Alternate proof of sels 5387, requiring ax-sep 5231 but not using el 5385 (which is proved from it as elALT 5389). (especially when the proof of el 5385 is inlined in sels 5387). (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5389. (Revised by BJ, 3-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	elALT 5389*	Alternate proof of el 5385, shorter but requiring ax-sep 5231. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	snelpwg 5390	A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) Put in closed form and avoid ax-nul 5241. (Revised by BJ, 17-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
Theorem	snelpwi 5391	If a set is a member of a class, then the singleton of that set is a member of the powerclass of that class. (Contributed by Alan Sare, 25-Aug-2011.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)
Theorem	snelpw 5392	A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵)
Theorem	prelpw 5393	An unordered pair of two sets is a member of the powerclass of a class if and only if the two sets are members of that class. (Contributed by AV, 8-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
Theorem	prelpwi 5394	If two sets are members of a class, then the unordered pair of those two sets is a member of the powerclass of that class. (Contributed by Thierry Arnoux, 10-Mar-2017.) (Proof shortened by AV, 23-Oct-2021.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)
Theorem	rext 5395*	A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.)
⊢ (∀𝑧(𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)
Theorem	sspwb 5396	The powerclass construction preserves and reflects inclusion. Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)
Theorem	unipw 5397	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.)
⊢ ∪ 𝒫 𝐴 = 𝐴
Theorem	univ 5398	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	pwtr 5399	A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.)
⊢ (Tr 𝐴 ↔ Tr 𝒫 𝐴)
Theorem	ssextss 5400*	An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))