Metamath Proof Explorer

Theorem sbcoteq1a

Description: Equality theorem for substitution of a class for an ordered triple. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Assertion sbcoteq1a 
|- ( A = <. x , y , z >. -> ( [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> ph ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = <. x , y , z >. -> ( 2nd ` A ) = ( 2nd ` <. x , y , z >. ) )
2 ot3rdg 
 |-  ( z e. _V -> ( 2nd ` <. x , y , z >. ) = z )
3 2 elv 
 |-  ( 2nd ` <. x , y , z >. ) = z
4 1 3 eqtr2di 
 |-  ( A = <. x , y , z >. -> z = ( 2nd ` A ) )
5 sbceq1a 
 |-  ( z = ( 2nd ` A ) -> ( ph <-> [. ( 2nd ` A ) / z ]. ph ) )
6 4 5 syl 
 |-  ( A = <. x , y , z >. -> ( ph <-> [. ( 2nd ` A ) / z ]. ph ) )
7 2fveq3 
 |-  ( A = <. x , y , z >. -> ( 2nd ` ( 1st ` A ) ) = ( 2nd ` ( 1st ` <. x , y , z >. ) ) )
8 vex 
 |-  x e. _V
9 vex 
 |-  y e. _V
10 vex 
 |-  z e. _V
11 ot2ndg 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( 2nd ` ( 1st ` <. x , y , z >. ) ) = y )
12 8 9 10 11 mp3an 
 |-  ( 2nd ` ( 1st ` <. x , y , z >. ) ) = y
13 7 12 eqtr2di 
 |-  ( A = <. x , y , z >. -> y = ( 2nd ` ( 1st ` A ) ) )
14 sbceq1a 
 |-  ( y = ( 2nd ` ( 1st ` A ) ) -> ( [. ( 2nd ` A ) / z ]. ph <-> [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) )
15 13 14 syl 
 |-  ( A = <. x , y , z >. -> ( [. ( 2nd ` A ) / z ]. ph <-> [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) )
16 2fveq3 
 |-  ( A = <. x , y , z >. -> ( 1st ` ( 1st ` A ) ) = ( 1st ` ( 1st ` <. x , y , z >. ) ) )
17 ot1stg 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( 1st ` ( 1st ` <. x , y , z >. ) ) = x )
18 8 9 10 17 mp3an 
 |-  ( 1st ` ( 1st ` <. x , y , z >. ) ) = x
19 16 18 eqtr2di 
 |-  ( A = <. x , y , z >. -> x = ( 1st ` ( 1st ` A ) ) )
20 sbceq1a 
 |-  ( x = ( 1st ` ( 1st ` A ) ) -> ( [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) )
21 19 20 syl 
 |-  ( A = <. x , y , z >. -> ( [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) )
22 6 15 21 3bitrrd 
 |-  ( A = <. x , y , z >. -> ( [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> ph ) )