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

Metamath Proof Explorer

Theorem sbcopeq1a

Description: Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a that avoids the existential quantifiers of copsexg ). (Contributed by NM, 19-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

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

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 sbceq1a 
 |-  ( y = ( 2nd ` A ) -> ( ph <-> [. ( 2nd ` A ) / y ]. ph ) )
6 4 5 syl 
 |-  ( A = <. x , y >. -> ( ph <-> [. ( 2nd ` A ) / y ]. ph ) )
7 1 2 op1std 
 |-  ( A = <. x , y >. -> ( 1st ` A ) = x )
8 7 eqcomd 
 |-  ( A = <. x , y >. -> x = ( 1st ` A ) )
9 sbceq1a 
 |-  ( x = ( 1st ` A ) -> ( [. ( 2nd ` A ) / y ]. ph <-> [. ( 1st ` A ) / x ]. [. ( 2nd ` A ) / y ]. ph ) )
10 8 9 syl 
 |-  ( A = <. x , y >. -> ( [. ( 2nd ` A ) / y ]. ph <-> [. ( 1st ` A ) / x ]. [. ( 2nd ` A ) / y ]. ph ) )
11 6 10 bitr2d 
 |-  ( A = <. x , y >. -> ( [. ( 1st ` A ) / x ]. [. ( 2nd ` A ) / y ]. ph <-> ph ) )