Theorem axprALT

Description: Alternate proof of axpr . (Contributed by NM, 14-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	axprALT	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		zfpair	⊢ { 𝑥 , 𝑦 } ∈ V
2	1	isseti	⊢ ∃ 𝑧 𝑧 = { 𝑥 , 𝑦 }
3		dfcleq	⊢ ( 𝑧 = { 𝑥 , 𝑦 } ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ { 𝑥 , 𝑦 } ) )
4		vex	⊢ 𝑤 ∈ V
5	4	elpr	⊢ ( 𝑤 ∈ { 𝑥 , 𝑦 } ↔ ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) )
6	5	bibi2i	⊢ ( ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ { 𝑥 , 𝑦 } ) ↔ ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) ) )
7		biimpr	⊢ ( ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) )
8	6 7	sylbi	⊢ ( ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ { 𝑥 , 𝑦 } ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) )
9	8	alimi	⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ { 𝑥 , 𝑦 } ) → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) )
10	3 9	sylbi	⊢ ( 𝑧 = { 𝑥 , 𝑦 } → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) )
11	2 10	eximii	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )