Metamath Proof Explorer

Theorem oteqex

Description: Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 28-May-2008) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. _V /\ B e. _V /\ C e. _V ) -> C e. _V )
2 1 a1i 
 |-  ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( ( A e. _V /\ B e. _V /\ C e. _V ) -> C e. _V ) )
3 simp3 
 |-  ( ( R e. _V /\ S e. _V /\ T e. _V ) -> T e. _V )
4 oteqex2 
 |-  ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( C e. _V <-> T e. _V ) )
5 3 4 imbitrrid 
 |-  ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( ( R e. _V /\ S e. _V /\ T e. _V ) -> C e. _V ) )
6 opex 
 |-  <. A , B >. e. _V
7 opthg 
 |-  ( ( <. A , B >. e. _V /\ C e. _V ) -> ( <. <. A , B >. , C >. = <. <. R , S >. , T >. <-> ( <. A , B >. = <. R , S >. /\ C = T ) ) )
8 6 7 mpan 
 |-  ( C e. _V -> ( <. <. A , B >. , C >. = <. <. R , S >. , T >. <-> ( <. A , B >. = <. R , S >. /\ C = T ) ) )
9 8 simprbda 
 |-  ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> <. A , B >. = <. R , S >. )
10 opeqex 
 |-  ( <. A , B >. = <. R , S >. -> ( ( A e. _V /\ B e. _V ) <-> ( R e. _V /\ S e. _V ) ) )
11 9 10 syl 
 |-  ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> ( ( A e. _V /\ B e. _V ) <-> ( R e. _V /\ S e. _V ) ) )
12 4 adantl 
 |-  ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> ( C e. _V <-> T e. _V ) )
13 11 12 anbi12d 
 |-  ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> ( ( ( A e. _V /\ B e. _V ) /\ C e. _V ) <-> ( ( R e. _V /\ S e. _V ) /\ T e. _V ) ) )
14 df-3an 
 |-  ( ( A e. _V /\ B e. _V /\ C e. _V ) <-> ( ( A e. _V /\ B e. _V ) /\ C e. _V ) )
15 df-3an 
 |-  ( ( R e. _V /\ S e. _V /\ T e. _V ) <-> ( ( R e. _V /\ S e. _V ) /\ T e. _V ) )
16 13 14 15 3bitr4g 
 |-  ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> ( ( A e. _V /\ B e. _V /\ C e. _V ) <-> ( R e. _V /\ S e. _V /\ T e. _V ) ) )
17 16 expcom 
 |-  ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( C e. _V -> ( ( A e. _V /\ B e. _V /\ C e. _V ) <-> ( R e. _V /\ S e. _V /\ T e. _V ) ) ) )
18 2 5 17 pm5.21ndd 
 |-  ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( ( A e. _V /\ B e. _V /\ C e. _V ) <-> ( R e. _V /\ S e. _V /\ T e. _V ) ) )