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 ) )