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	$⊢ ⟨A, B⟩ \neq \emptyset \leftrightarrow (A \in V \land B \in V)$

Step	Hyp	Ref	Expression
1		opprc	$⊢ \neg (A \in V \land B \in V) \to ⟨A, B⟩ = \emptyset$
2	1	necon1ai	$⊢ ⟨A, B⟩ \neq \emptyset \to (A \in V \land B \in V)$
3		dfopg	$⊢ (A \in V \land B \in V) \to ⟨A, B⟩ = \{\{A\}, \{A, B\}\}$
4		snex	$⊢ \{A\} \in V$
5	4	prnz	$⊢ \{\{A\}, \{A, B\}\} \neq \emptyset$
6	5	a1i	$⊢ (A \in V \land B \in V) \to \{\{A\}, \{A, B\}\} \neq \emptyset$
7	3 6	eqnetrd	$⊢ (A \in V \land B \in V) \to ⟨A, B⟩ \neq \emptyset$
8	2 7	impbii	$⊢ ⟨A, B⟩ \neq \emptyset \leftrightarrow (A \in V \land B \in V)$

Metamath Proof Explorer