Metamath Proof Explorer


Theorem eloprabgaOLD

Description: Obsolete version of eloprabga as of 15-Oct-2024. (Contributed by NM, 14-Sep-1999) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 19-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis eloprabga.1
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
Assertion eloprabgaOLD
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) )

Proof

Step Hyp Ref Expression
1 eloprabga.1
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
2 elex
 |-  ( A e. V -> A e. _V )
3 elex
 |-  ( B e. W -> B e. _V )
4 elex
 |-  ( C e. X -> C e. _V )
5 opex
 |-  <. <. A , B >. , C >. e. _V
6 simpr
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> w = <. <. A , B >. , C >. )
7 6 eqeq1d
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> ( w = <. <. x , y >. , z >. <-> <. <. A , B >. , C >. = <. <. x , y >. , z >. ) )
8 eqcom
 |-  ( <. <. A , B >. , C >. = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. A , B >. , C >. )
9 vex
 |-  x e. _V
10 vex
 |-  y e. _V
11 vex
 |-  z e. _V
12 9 10 11 otth2
 |-  ( <. <. x , y >. , z >. = <. <. A , B >. , C >. <-> ( x = A /\ y = B /\ z = C ) )
13 8 12 bitri
 |-  ( <. <. A , B >. , C >. = <. <. x , y >. , z >. <-> ( x = A /\ y = B /\ z = C ) )
14 7 13 bitrdi
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> ( w = <. <. x , y >. , z >. <-> ( x = A /\ y = B /\ z = C ) ) )
15 14 anbi1d
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( ( x = A /\ y = B /\ z = C ) /\ ph ) ) )
16 1 pm5.32i
 |-  ( ( ( x = A /\ y = B /\ z = C ) /\ ph ) <-> ( ( x = A /\ y = B /\ z = C ) /\ ps ) )
17 15 16 bitrdi
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( ( x = A /\ y = B /\ z = C ) /\ ps ) ) )
18 17 3exbidv
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> E. x E. y E. z ( ( x = A /\ y = B /\ z = C ) /\ ps ) ) )
19 df-oprab
 |-  { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
20 19 eleq2i
 |-  ( w e. { <. <. x , y >. , z >. | ph } <-> w e. { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) } )
21 abid
 |-  ( w e. { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) } <-> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
22 20 21 bitr2i
 |-  ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> w e. { <. <. x , y >. , z >. | ph } )
23 eleq1
 |-  ( w = <. <. A , B >. , C >. -> ( w e. { <. <. x , y >. , z >. | ph } <-> <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } ) )
24 22 23 syl5bb
 |-  ( w = <. <. A , B >. , C >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } ) )
25 24 adantl
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } ) )
26 19.41vvv
 |-  ( E. x E. y E. z ( ( x = A /\ y = B /\ z = C ) /\ ps ) <-> ( E. x E. y E. z ( x = A /\ y = B /\ z = C ) /\ ps ) )
27 elisset
 |-  ( A e. _V -> E. x x = A )
28 elisset
 |-  ( B e. _V -> E. y y = B )
29 elisset
 |-  ( C e. _V -> E. z z = C )
30 27 28 29 3anim123i
 |-  ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( E. x x = A /\ E. y y = B /\ E. z z = C ) )
31 eeeanv
 |-  ( E. x E. y E. z ( x = A /\ y = B /\ z = C ) <-> ( E. x x = A /\ E. y y = B /\ E. z z = C ) )
32 30 31 sylibr
 |-  ( ( A e. _V /\ B e. _V /\ C e. _V ) -> E. x E. y E. z ( x = A /\ y = B /\ z = C ) )
33 32 biantrurd
 |-  ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( ps <-> ( E. x E. y E. z ( x = A /\ y = B /\ z = C ) /\ ps ) ) )
34 26 33 bitr4id
 |-  ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( E. x E. y E. z ( ( x = A /\ y = B /\ z = C ) /\ ps ) <-> ps ) )
35 34 adantr
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> ( E. x E. y E. z ( ( x = A /\ y = B /\ z = C ) /\ ps ) <-> ps ) )
36 18 25 35 3bitr3d
 |-  ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ w = <. <. A , B >. , C >. ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) )
37 36 expcom
 |-  ( w = <. <. A , B >. , C >. -> ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) ) )
38 5 37 vtocle
 |-  ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) )
39 2 3 4 38 syl3an
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) )