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

Metamath Proof Explorer

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 ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 )