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 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥𝑦 𝜑 )