This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zfpair2

Description: Derive the abbreviated version of the Axiom of Pairing from ax-pr . See zfpair for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006)

		Ref	Expression
	Assertion	zfpair2	⊢ { 𝑥 , 𝑦 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		ax-pr	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )
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