Metamath Proof Explorer


Theorem opnz

Description: An ordered pair is nonempty iff the arguments are sets. (Contributed by NM, 24-Jan-2004) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion opnz ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step Hyp Ref Expression
1 opprc ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
2 1 necon1ai ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3 dfopg ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
4 snex { 𝐴 } ∈ V
5 4 prnz { { 𝐴 } , { 𝐴 , 𝐵 } } ≠ ∅
6 5 a1i ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ≠ ∅ )
7 3 6 eqnetrd ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ )
8 2 7 impbii ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )