prex

Description: 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 ), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993) Avoid ax-nul and shorten proof. (Revised by GG, 6-Mar-2026)

		Ref	Expression
	Assertion	prex	⊢ { 𝐴 , 𝐵 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		axprg	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → 𝑤 ∈ 𝑧 )
2	1	sepexi	⊢ ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) )
3		dfcleq	⊢ ( 𝑧 = { 𝐴 , 𝐵 } ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ { 𝐴 , 𝐵 } ) )
4		vex	⊢ 𝑤 ∈ V
5	4	elpr	⊢ ( 𝑤 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) )
6	5	bibi2i	⊢ ( ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ { 𝐴 , 𝐵 } ) ↔ ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) ) )
7	6	albii	⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ { 𝐴 , 𝐵 } ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) ) )
8	3 7	bitri	⊢ ( 𝑧 = { 𝐴 , 𝐵 } ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) ) )
9	8	exbii	⊢ ( ∃ 𝑧 𝑧 = { 𝐴 , 𝐵 } ↔ ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) ) )
10	2 9	mpbir	⊢ ∃ 𝑧 𝑧 = { 𝐴 , 𝐵 }
11	10	issetri	⊢ { 𝐴 , 𝐵 } ∈ V

Metamath Proof Explorer

Theorem prex

Proof