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 syl5ibr
 |-  ( <. <. 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 ) ) )