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 >. -> ( ( A e. _V /\ B e. _V ) <-> ( C e. _V /\ D e. _V ) ) )

Proof

Step	Hyp	Ref	Expression
1		neeq1	|- ( <. A , B >. = <. C , D >. -> ( <. A , B >. =/= (/) <-> <. C , D >. =/= (/) ) )
2		opnz	|- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )
3		opnz	|- ( <. C , D >. =/= (/) <-> ( C e. _V /\ D e. _V ) )
4	1 2 3	3bitr3g	|- ( <. A , B >. = <. C , D >. -> ( ( A e. _V /\ B e. _V ) <-> ( C e. _V /\ D e. _V ) ) )