Metamath Proof Explorer

Theorem opsbc2ie

Description: Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023)

Ref Expression
Hypothesis opsbc2ie.a 
|- ( p = <. a , b >. -> ( ph <-> ch ) )
Assertion opsbc2ie 
|- ( p = <. x , y >. -> ( ph <-> [. y / b ]. [. x / a ]. ch ) )

Proof

Step Hyp Ref Expression
1 opsbc2ie.a 
 |-  ( p = <. a , b >. -> ( ph <-> ch ) )
2 1 sbcth 
 |-  ( x e. _V -> [. x / a ]. ( p = <. a , b >. -> ( ph <-> ch ) ) )
3 sbcim1 
 |-  ( [. x / a ]. ( p = <. a , b >. -> ( ph <-> ch ) ) -> ( [. x / a ]. p = <. a , b >. -> [. x / a ]. ( ph <-> ch ) ) )
4 2 3 syl 
 |-  ( x e. _V -> ( [. x / a ]. p = <. a , b >. -> [. x / a ]. ( ph <-> ch ) ) )
5 sbceq2g 
 |-  ( x e. _V -> ( [. x / a ]. p = <. a , b >. <-> p = [_ x / a ]_ <. a , b >. ) )
6 csbopg 
 |-  ( x e. _V -> [_ x / a ]_ <. a , b >. = <. [_ x / a ]_ a , [_ x / a ]_ b >. )
7 csbvarg 
 |-  ( x e. _V -> [_ x / a ]_ a = x )
8 csbconstg 
 |-  ( x e. _V -> [_ x / a ]_ b = b )
9 7 8 opeq12d 
 |-  ( x e. _V -> <. [_ x / a ]_ a , [_ x / a ]_ b >. = <. x , b >. )
10 6 9 eqtrd 
 |-  ( x e. _V -> [_ x / a ]_ <. a , b >. = <. x , b >. )
11 10 eqeq2d 
 |-  ( x e. _V -> ( p = [_ x / a ]_ <. a , b >. <-> p = <. x , b >. ) )
12 5 11 bitrd 
 |-  ( x e. _V -> ( [. x / a ]. p = <. a , b >. <-> p = <. x , b >. ) )
13 sbcbig 
 |-  ( x e. _V -> ( [. x / a ]. ( ph <-> ch ) <-> ( [. x / a ]. ph <-> [. x / a ]. ch ) ) )
14 sbcg 
 |-  ( x e. _V -> ( [. x / a ]. ph <-> ph ) )
15 14 bibi1d 
 |-  ( x e. _V -> ( ( [. x / a ]. ph <-> [. x / a ]. ch ) <-> ( ph <-> [. x / a ]. ch ) ) )
16 13 15 bitrd 
 |-  ( x e. _V -> ( [. x / a ]. ( ph <-> ch ) <-> ( ph <-> [. x / a ]. ch ) ) )
17 4 12 16 3imtr3d 
 |-  ( x e. _V -> ( p = <. x , b >. -> ( ph <-> [. x / a ]. ch ) ) )
18 17 elv 
 |-  ( p = <. x , b >. -> ( ph <-> [. x / a ]. ch ) )
19 18 sbcth 
 |-  ( y e. _V -> [. y / b ]. ( p = <. x , b >. -> ( ph <-> [. x / a ]. ch ) ) )
20 sbcim1 
 |-  ( [. y / b ]. ( p = <. x , b >. -> ( ph <-> [. x / a ]. ch ) ) -> ( [. y / b ]. p = <. x , b >. -> [. y / b ]. ( ph <-> [. x / a ]. ch ) ) )
21 19 20 syl 
 |-  ( y e. _V -> ( [. y / b ]. p = <. x , b >. -> [. y / b ]. ( ph <-> [. x / a ]. ch ) ) )
22 sbceq2g 
 |-  ( y e. _V -> ( [. y / b ]. p = <. x , b >. <-> p = [_ y / b ]_ <. x , b >. ) )
23 csbopg 
 |-  ( y e. _V -> [_ y / b ]_ <. x , b >. = <. [_ y / b ]_ x , [_ y / b ]_ b >. )
24 csbconstg 
 |-  ( y e. _V -> [_ y / b ]_ x = x )
25 csbvarg 
 |-  ( y e. _V -> [_ y / b ]_ b = y )
26 24 25 opeq12d 
 |-  ( y e. _V -> <. [_ y / b ]_ x , [_ y / b ]_ b >. = <. x , y >. )
27 23 26 eqtrd 
 |-  ( y e. _V -> [_ y / b ]_ <. x , b >. = <. x , y >. )
28 27 eqeq2d 
 |-  ( y e. _V -> ( p = [_ y / b ]_ <. x , b >. <-> p = <. x , y >. ) )
29 22 28 bitrd 
 |-  ( y e. _V -> ( [. y / b ]. p = <. x , b >. <-> p = <. x , y >. ) )
30 sbcbig 
 |-  ( y e. _V -> ( [. y / b ]. ( ph <-> [. x / a ]. ch ) <-> ( [. y / b ]. ph <-> [. y / b ]. [. x / a ]. ch ) ) )
31 sbcg 
 |-  ( y e. _V -> ( [. y / b ]. ph <-> ph ) )
32 31 bibi1d 
 |-  ( y e. _V -> ( ( [. y / b ]. ph <-> [. y / b ]. [. x / a ]. ch ) <-> ( ph <-> [. y / b ]. [. x / a ]. ch ) ) )
33 30 32 bitrd 
 |-  ( y e. _V -> ( [. y / b ]. ( ph <-> [. x / a ]. ch ) <-> ( ph <-> [. y / b ]. [. x / a ]. ch ) ) )
34 21 29 33 3imtr3d 
 |-  ( y e. _V -> ( p = <. x , y >. -> ( ph <-> [. y / b ]. [. x / a ]. ch ) ) )
35 34 elv 
 |-  ( p = <. x , y >. -> ( ph <-> [. y / b ]. [. x / a ]. ch ) )