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

Metamath Proof Explorer

Theorem opabn0

Description: Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007)

Ref Expression
Assertion opabn0 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
2 elopab ⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
3 2 exbii ⊢ ( ∃ 𝑧 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
4 exrot3 ⊢ ( ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
5 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
6 5 isseti ⊢ ∃ 𝑧 𝑧 = ⟨ 𝑥 , 𝑦 ⟩
7 19.41v ⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ∃ 𝑧 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
8 6 7 mpbiran ⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜑 )
9 8 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )
10 4 9 bitri ⊢ ( ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )
11 3 10 bitri ⊢ ( ∃ 𝑧 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )
12 1 11 bitri ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )