Metamath Proof Explorer

Theorem opeqex

Description: Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008)

		Ref	Expression
	Assertion	opeqex	$⊢ ⟨A, B⟩ = ⟨C, D⟩ \to ((A \in V \land B \in V) \leftrightarrow (C \in V \land D \in V))$

Step	Hyp	Ref	Expression
1		neeq1	$⊢ ⟨A, B⟩ = ⟨C, D⟩ \to (⟨A, B⟩ \neq \emptyset \leftrightarrow ⟨C, D⟩ \neq \emptyset)$
2		opnz	$⊢ ⟨A, B⟩ \neq \emptyset \leftrightarrow (A \in V \land B \in V)$
3		opnz	$⊢ ⟨C, D⟩ \neq \emptyset \leftrightarrow (C \in V \land D \in V)$
4	1 2 3	3bitr3g	$⊢ ⟨A, B⟩ = ⟨C, D⟩ \to ((A \in V \land B \in V) \leftrightarrow (C \in V \land D \in V))$