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 ) )