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