Theorem oteqex2

Description: Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 26-Apr-2015)

	Ref	Expression
Assertion	oteqex2	|- ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( C e. _V <-> T e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		opeqex	|- ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( ( <. A , B >. e. _V /\ C e. _V ) <-> ( <. R , S >. e. _V /\ T e. _V ) ) )
2		opex	|- <. A , B >. e. _V
3	2	biantrur	|- ( C e. _V <-> ( <. A , B >. e. _V /\ C e. _V ) )
4		opex	|- <. R , S >. e. _V
5	4	biantrur	|- ( T e. _V <-> ( <. R , S >. e. _V /\ T e. _V ) )
6	1 3 5	3bitr4g	|- ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( C e. _V <-> T e. _V ) )