This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbopeq1a

Description: Equality theorem for substitution of a class A for an ordered pair <. x , y >. in B (analogue of csbeq1a ). (Contributed by NM, 19-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion csbopeq1a 
|- ( A = <. x , y >. -> [_ ( 1st ` A ) / x ]_ [_ ( 2nd ` A ) / y ]_ B = B )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 1 2 op2ndd 
 |-  ( A = <. x , y >. -> ( 2nd ` A ) = y )
4 3 eqcomd 
 |-  ( A = <. x , y >. -> y = ( 2nd ` A ) )
5 csbeq1a 
 |-  ( y = ( 2nd ` A ) -> B = [_ ( 2nd ` A ) / y ]_ B )
6 4 5 syl 
 |-  ( A = <. x , y >. -> B = [_ ( 2nd ` A ) / y ]_ B )
7 1 2 op1std 
 |-  ( A = <. x , y >. -> ( 1st ` A ) = x )
8 7 eqcomd 
 |-  ( A = <. x , y >. -> x = ( 1st ` A ) )
9 csbeq1a 
 |-  ( x = ( 1st ` A ) -> [_ ( 2nd ` A ) / y ]_ B = [_ ( 1st ` A ) / x ]_ [_ ( 2nd ` A ) / y ]_ B )
10 8 9 syl 
 |-  ( A = <. x , y >. -> [_ ( 2nd ` A ) / y ]_ B = [_ ( 1st ` A ) / x ]_ [_ ( 2nd ` A ) / y ]_ B )
11 6 10 eqtr2d 
 |-  ( A = <. x , y >. -> [_ ( 1st ` A ) / x ]_ [_ ( 2nd ` A ) / y ]_ B = B )