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

Metamath Proof Explorer

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