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		opex	|- <. x , y >. e. _V
2		vex	|- z e. _V
3	1 2	op2ndd	|- ( A = <. <. x , y >. , z >. -> ( 2nd ` A ) = z )
4	3	eqcomd	|- ( 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		vex	|- x e. _V
8		vex	|- y e. _V
9	7 8 2	ot22ndd	|- ( A = <. <. x , y >. , z >. -> ( 2nd ` ( 1st ` A ) ) = y )
10	9	eqcomd	|- ( A = <. <. x , y >. , z >. -> y = ( 2nd ` ( 1st ` A ) ) )
11		sbceq1a	|- ( y = ( 2nd ` ( 1st ` A ) ) -> ( [. ( 2nd ` A ) / z ]. ph <-> [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) )
12	10 11	syl	|- ( A = <. <. x , y >. , z >. -> ( [. ( 2nd ` A ) / z ]. ph <-> [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph ) )
13	7 8 2	ot21std	|- ( A = <. <. x , y >. , z >. -> ( 1st ` ( 1st ` A ) ) = x )
14	13	eqcomd	|- ( A = <. <. x , y >. , z >. -> x = ( 1st ` ( 1st ` A ) ) )
15		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 ) )
16	14 15	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 ) )
17	6 12 16	3bitrrd	|- ( A = <. <. x , y >. , z >. -> ( [. ( 1st ` ( 1st ` A ) ) / x ]. [. ( 2nd ` ( 1st ` A ) ) / y ]. [. ( 2nd ` A ) / z ]. ph <-> ph ) )