Theorem sbcop1

Description: The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of its first component. (Contributed by AV, 8-Apr-2023)

	Ref	Expression
Hypothesis	sbcop.z	|- ( z = <. x , y >. -> ( ph <-> ps ) )
Assertion	sbcop1	|- ( [. a / x ]. ps <-> [. <. a , y >. / z ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbcop.z	|- ( z = <. x , y >. -> ( ph <-> ps ) )
2		sbc5	|- ( [. a / x ]. ps <-> E. x ( x = a /\ ps ) )
3		opeq1	|- ( a = x -> <. a , y >. = <. x , y >. )
4	3	equcoms	|- ( x = a -> <. a , y >. = <. x , y >. )
5	4	eqeq2d	|- ( x = a -> ( z = <. a , y >. <-> z = <. x , y >. ) )
6	1	biimprd	|- ( z = <. x , y >. -> ( ps -> ph ) )
7	5 6	syl6bi	|- ( x = a -> ( z = <. a , y >. -> ( ps -> ph ) ) )
8	7	com23	|- ( x = a -> ( ps -> ( z = <. a , y >. -> ph ) ) )
9	8	imp	|- ( ( x = a /\ ps ) -> ( z = <. a , y >. -> ph ) )
10	9	exlimiv	|- ( E. x ( x = a /\ ps ) -> ( z = <. a , y >. -> ph ) )
11	2 10	sylbi	|- ( [. a / x ]. ps -> ( z = <. a , y >. -> ph ) )
12	11	alrimiv	|- ( [. a / x ]. ps -> A. z ( z = <. a , y >. -> ph ) )
13		opex	|- <. a , y >. e. _V
14	13	sbc6	|- ( [. <. a , y >. / z ]. ph <-> A. z ( z = <. a , y >. -> ph ) )
15	12 14	sylibr	|- ( [. a / x ]. ps -> [. <. a , y >. / z ]. ph )
16		sbc5	|- ( [. <. a , y >. / z ]. ph <-> E. z ( z = <. a , y >. /\ ph ) )
17	1	biimpd	|- ( z = <. x , y >. -> ( ph -> ps ) )
18	5 17	syl6bi	|- ( x = a -> ( z = <. a , y >. -> ( ph -> ps ) ) )
19	18	com3l	|- ( z = <. a , y >. -> ( ph -> ( x = a -> ps ) ) )
20	19	imp	|- ( ( z = <. a , y >. /\ ph ) -> ( x = a -> ps ) )
21	20	alrimiv	|- ( ( z = <. a , y >. /\ ph ) -> A. x ( x = a -> ps ) )
22		vex	|- a e. _V
23	22	sbc6	|- ( [. a / x ]. ps <-> A. x ( x = a -> ps ) )
24	21 23	sylibr	|- ( ( z = <. a , y >. /\ ph ) -> [. a / x ]. ps )
25	24	exlimiv	|- ( E. z ( z = <. a , y >. /\ ph ) -> [. a / x ]. ps )
26	16 25	sylbi	|- ( [. <. a , y >. / z ]. ph -> [. a / x ]. ps )
27	15 26	impbii	|- ( [. a / x ]. ps <-> [. <. a , y >. / z ]. ph )