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	difexg 5301	Existence of a difference. (Contributed by NM, 26-May-1998.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)
Theorem	difexi 5302	Existence of a difference, inference version of difexg 5301. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∖ 𝐵) ∈ V
Theorem	difexd 5303	Existence of a difference. (Contributed by SN, 16-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V)
Theorem	sepab 5304*	Separation Scheme (Aussonderung) in terms of a class abstraction. Prefer using the more natural statement rabexg 5309. (Contributed by NM, 8-Jun-1994.) Put in closed form. (Revised by BJ, 18-Jul-2026.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V)
Theorem	elpw2g 5305	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	elpw2 5306	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	elpwi2 5307	Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)
⊢ 𝐵 ∈ 𝑉    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ 𝒫 𝐵
Theorem	rabelpw 5308*	A restricted class abstraction is an element of the power set of its restricting set. (Contributed by AV, 9-Oct-2023.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ 𝒫 𝐴)
Theorem	rabexg 5309*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) (Proof shortened by BJ, 24-Jul-2025.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabexgOLD 5310*	Obsolete version of rabexg 5309 as of 24-Jul-2025). (Contributed by NM, 23-Oct-1999.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabex 5311*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V
Theorem	rabexd 5312*	Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5313. (Contributed by AV, 16-Jul-2019.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	rabex2 5313*	Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐵 ∈ V
Theorem	rab2ex 5314*	A class abstraction based on a class abstraction based on a set is a set. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
⊢ 𝐵 = {𝑦 ∈ 𝐴 ∣ 𝜓}    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} ∈ V
Theorem	elssabg 5315*	Membership in a class abstraction involving a subset. Unlike elabg 3636, 𝐴 does not have to be a set. (Contributed by NM, 29-Aug-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝜑)} ↔ (𝐴 ⊆ 𝐵 ∧ 𝜓)))
Theorem	intex 5316	The intersection of a nonempty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
Theorem	intnex 5317	If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005.)
⊢ (¬ ∩ 𝐴 ∈ V ↔ ∩ 𝐴 = V)
Theorem	intexab 5318	The intersection of a nonempty class abstraction exists. (Contributed by NM, 21-Oct-2003.)
⊢ (∃𝑥𝜑 ↔ ∩ {𝑥 ∣ 𝜑} ∈ V)
Theorem	intexrab 5319	The intersection of a nonempty restricted class abstraction exists. (Contributed by NM, 21-Oct-2003.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∩ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	iinexg 5320*	The existence of a class intersection. 𝑥 is normally a free-variable parameter in 𝐵, which should be read 𝐵(𝑥). (Contributed by FL, 19-Sep-2011.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	intabs 5321*	Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = ∩ {𝑦 ∣ 𝜓} → (𝜑 ↔ 𝜒))    &   ⊢ (∩ {𝑦 ∣ 𝜓} ⊆ 𝐴 ∧ 𝜒)    ⇒   ⊢ ∩ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑}
Theorem	inuni 5322*	The intersection of a union ∪ 𝐴 with a class 𝐵 is equal to the union of the intersections of each element of 𝐴 with 𝐵. (Contributed by FL, 24-Mar-2007.) (Proof shortened by Wolf Lammen, 15-May-2025.)
⊢ (∪ 𝐴 ∩ 𝐵) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)}
Theorem	axpweq 5323*	Two equivalent ways to express the Power Set Axiom. Note that ax-pow 5338 is not used by the proof. When ax-pow 5338 is assumed and 𝐴 is a set, both sides of the biconditional hold. In ZF, both sides hold if and only if 𝐴 is a set (see pwexr 7765). (Contributed by NM, 22-Jun-2009.)
⊢ (𝒫 𝐴 ∈ V ↔ ∃𝑥∀𝑦(∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝑥))
Theorem	pwnss 5324	The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Proof shortened by BJ, 24-Jul-2025.)
⊢ (𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴)
Theorem	pwne 5325	No set equals its power set. The sethood antecedent is necessary; compare pwv 4870. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ≠ 𝐴)
Theorem	difelpw 5326	A difference is an element of the power set of its minuend. (Contributed by AV, 9-Oct-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ 𝒫 𝐴)
2.2.5  Theorems requiring empty set existence
Theorem	class2set 5327*	The class of elements of 𝐴 "such that 𝐴 is a set" is a set. That class is equal to 𝐴 when 𝐴 is a set (see class2seteq 3668) and to the empty set when 𝐴 is a proper class. (Contributed by NM, 16-Oct-2003.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V} ∈ V
Theorem	0elpw 5328	Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
⊢ ∅ ∈ 𝒫 𝐴
Theorem	pwne0 5329	A power class is never empty. (Contributed by NM, 3-Sep-2018.)
⊢ 𝒫 𝐴 ≠ ∅
Theorem	0nep0 5330	The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
⊢ ∅ ≠ {∅}
Theorem	0inp0 5331	Something cannot be equal to both the empty set and the power set of the empty set. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 = ∅ → ¬ 𝐴 = {∅})
Theorem	unidif0 5332	The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) (Proof shortened by Eric Schmidt, 25-Apr-2026.)
⊢ ∪ (𝐴 ∖ {∅}) = ∪ 𝐴
Theorem	unidif0OLD 5333	Obsolete version of unidif0 5332 as of 25-Apr-2026. (Contributed by NM, 22-Mar-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∪ (𝐴 ∖ {∅}) = ∪ 𝐴
Theorem	eqsnuniex 5334	If a class is equal to the singleton of its union, then its union exists. (Contributed by BTernaryTau, 24-Sep-2024.)
⊢ (𝐴 = {∪ 𝐴} → ∪ 𝐴 ∈ V)
Theorem	iin0 5335*	An indexed intersection of the empty set, with a nonempty index set, is empty. (Contributed by NM, 20-Oct-2005.)
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝑥 ∈ 𝐴 ∅ = ∅)
Theorem	notsep 5336*	In the Separation Scheme sepgi 5261, we require that 𝑦 not occur in 𝜑 (which can be generalized to "not be free in"). That requirement is necessary: notsep 5336, which requires only ax-ext 2735 and ax-nul 5270 on top of first-order logic, derives *non*-existence of a "separating set" for specific values of the containing set 𝐴 and of the separating condition 𝜑. Therefore, from the axioms required by notsep 5336 and an overly strong axiom of separation without the requirement that 𝑦 not occur in 𝜑, we could derive ⊥, a contradiction. (Contributed by NM, 8-Feb-2006.) (Proof shortened by BJ, 18-Nov-2023.)
⊢ 𝐴 = {∅}    &   ⊢ (𝜑 ↔ ¬ 𝑥 ∈ 𝑦)    ⇒   ⊢ ¬ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	intv 5337	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 5338*	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 5340 uses explicit subset notation. A version using class notation is pwex 5353. (Contributed by NM, 21-Jun-1993.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfpow 5339*	Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpow2 5340*	A variant of the Axiom of Power Sets ax-pow 5338 using subset notation. Problem in [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)
Theorem	axpow3 5341*	A variant of the Axiom of Power Sets ax-pow 5338. 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 5342*	Alternate proof of el 5421 using ax-9 2153 and ax-pow 5338 instead of ax-pr 5406. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	dtruALT2 5343*	Alternate proof of dtru 5420 using ax-pow 5338 instead of ax-pr 5406. See dtruALT 5361 for another proof using ax-pow 5338 instead of ax-pr 5406. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2404. (Revised by BJ, 31-May-2019.) Avoid ax-12 2213. (Revised by Rohan Ridenour, 9-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	dtrucor 5344*	Corollary of dtru 5420. 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 5345. (Contributed by NM, 27-Jun-2002.)
⊢ 𝑥 = 𝑦    ⇒   ⊢ 𝑥 ≠ 𝑦
Theorem	dtrucor2 5345	The theorem form of the deduction dtrucor 5344 leads to a contradiction, as mentioned in the "Wrong!" example at mmdeduction.html#bad 5344. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 20-Oct-2007.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦)    ⇒   ⊢ (𝜑 ∧ ¬ 𝜑)
Theorem	dvdemo1 5346*	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 5347, 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 5347 for details on the "disjoint variable" mechanism. (The verb "bundle" to express this phenomenon was introduced by Raph Levien.) Note that dvdemo1 5346 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 2192 nor ax-13 2404. (Contributed by NM, 1-Dec-2006.) (Revised by BJ, 13-Jan-2024.)
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)
Theorem	dvdemo2 5347*	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 5346, 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 5346 for details on the "disjoint variable" mechanism. Note that dvdemo2 5347 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 2176, ax-11 2192, ax-12 2213, ax-13 2404. (Contributed by NM, 1-Dec-2006.) Avoid ax-13 2404. (Revised by BJ, 13-Jan-2024.)
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)
Theorem	nfnid 5348	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 5343 in its proof. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ ¬ Ⅎ𝑥𝑥
Theorem	nfcvb 5349	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 2404. (New usage is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	vpwex 5350	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 5351 from vpwex 5350. (Revised by BJ, 10-Aug-2022.)
⊢ 𝒫 𝑥 ∈ V
Theorem	pwexg 5351	Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
Theorem	pwexd 5352	Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
Theorem	pwex 5353	Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝒫 𝐴 ∈ V
Theorem	pwel 5354	Quantitative version of pwexg 5351: 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 5270 and ax-pr 5406 and shorten proof. (Revised by BJ, 13-Apr-2024.)
⊢ (𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 ∪ 𝐵)
Theorem	abssexg 5355*	Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V)
Theorem	snexALT 5356	Alternate proof of snex 5412 using Power Set (ax-pow 5338) instead of Pairing (ax-pr 5406). Unlike in the proof of zfpair 5394, Replacement (ax-rep 5239) 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 5357	The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5358. (Contributed by NM, 23-Dec-1993.)
⊢ {∅} ∈ V
Theorem	p0exALT 5358	Alternate proof of p0ex 5357 which is quite different and longer if snexALT 5356 is expanded. (Contributed by NM, 23-Dec-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {∅} ∈ V
Theorem	pp0ex 5359	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 5360	The ordinal number 3 is a set, proved without the Axiom of Union ax-un 7734. (Contributed by NM, 2-May-2009.)
⊢ {∅, {∅}, {∅, {∅}}} ∈ V
Theorem	dtruALT 5361*	Alternate proof of dtru 5420 which requires more axioms but is shorter and may be easier to understand. Like dtruALT2 5343, it uses ax-pow 5338 rather than ax-pr 5406. Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that 𝑥 and 𝑦 be distinct. Specifically, Theorem spcev 3566 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 5362*	This theorem shows that Axiom ax-c16 39647 is redundant in the presence of Theorem dtruALT2 5343, which states simply that at least two things exist. This justifies the remark at mmzfcnd.html#twoness 5343 (which links to this theorem). (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 7-Nov-2006.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	eunex 5363	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 5364*	Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.)
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ ∃𝑦∀𝑥 𝑦 = 𝐴)
Theorem	eusvnf 5365*	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 5366*	Two ways to say that 𝐴(𝑥) is a set expression that does not depend on 𝑥. (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V))
Theorem	eusv2i 5367*	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 5368*	Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by Mario Carneiro, 18-Nov-2016.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴)
Theorem	eusv2 5369*	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 5370*	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 5371*	Lemma for reusv2 5376. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ (𝐴 ≠ ∅ → (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	reusv2lem2 5372*	Lemma for reusv2 5376. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.)
⊢ (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵)
Theorem	reusv2lem3 5373*	Lemma for reusv2 5376. (Contributed by NM, 14-Dec-2012.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ (∀𝑦 ∈ 𝐴 𝐵 ∈ V → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	reusv2lem4 5374*	Lemma for reusv2 5376. (Contributed by NM, 13-Dec-2012.)
⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝐶))
Theorem	reusv2lem5 5375*	Lemma for reusv2 5376. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ ((∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 = 𝐶))
Theorem	reusv2 5376*	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 5377*	Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷))
Theorem	reusv3 5378*	Two ways to express single-valuedness of a class expression 𝐶(𝑦). See reusv1 5370 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    ⇒   ⊢ (∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝐶 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
Theorem	eusv4 5379*	Two ways to express single-valuedness of a class expression 𝐵(𝑦). (Contributed by NM, 27-Oct-2010.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)
Theorem	alxfr 5380*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 18-Feb-2007.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((∀𝑦 𝐴 ∈ 𝐵 ∧ ∀𝑥∃𝑦 𝑥 = 𝐴) → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	ralxfrd 5381*	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 5382*	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 5383*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))
Theorem	rexxfr2d 5384*	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 5385*	Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of ralxfrd 5381. (Contributed by Alexander van der Vekens, 25-Apr-2018.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))
Theorem	rexxfrd2 5386*	Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of rexxfrd 5382. (Contributed by Alexander van der Vekens, 25-Apr-2018.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒))
Theorem	ralxfr 5387*	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 5388*	Alternate proof of ralxfr 5387 which does not use ralxfrd 5381. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓)
Theorem	rexxfr 5389*	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 5390*	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 5391*	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 5392*	A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd 7403. (Contributed by NM, 16-Jan-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)
Theorem	reuhyp 5393*	A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr1 3716. (Contributed by NM, 15-Nov-2004.)
⊢ (𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶)    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵))    ⇒   ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)
Theorem	zfpair 5394	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 5395. Instead, use zfpair2 5407 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 5395*	Alternate proof of axpr 5400. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
2.3.2  Derive the Axiom of Pairing
Theorem	axprlem1 5396*	Lemma for axpr 5400. 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 5397*	Lemma for axpr 5400. 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 5398*	Lemma for axpr 5400. 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 5399*	Lemma for axpr 5400. 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 5400*	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 5406 below so that the uses of the Axiom of Pairing can be more easily identified. For a shorter proof using ax-ext 2735, see axprALT 5395. (Contributed by NM, 14-Nov-2006.) Remove dependency on ax-ext 2735. (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 5406 instead. (New usage is discouraged.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)