Metamath Proof Explorer

Theorem eloprabga

Description: The law of concretion for operation class abstraction. Compare elopab . (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)

Ref Expression
Hypothesis eloprabga.1 
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
Assertion eloprabga 
|- ( ( 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 ) )