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

Metamath Proof Explorer

Theorem sbcop

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

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

Proof

Step Hyp Ref Expression
1 sbcop.z 
 |-  ( z = <. x , y >. -> ( ph <-> ps ) )
2 1 sbcop1 
 |-  ( [. a / x ]. ps <-> [. <. a , y >. / z ]. ph )
3 2 sbcbii 
 |-  ( [. b / y ]. [. a / x ]. ps <-> [. b / y ]. [. <. a , y >. / z ]. ph )
4 sbcnestgw 
 |-  ( b e. _V -> ( [. b / y ]. [. <. a , y >. / z ]. ph <-> [. [_ b / y ]_ <. a , y >. / z ]. ph ) )
5 4 elv 
 |-  ( [. b / y ]. [. <. a , y >. / z ]. ph <-> [. [_ b / y ]_ <. a , y >. / z ]. ph )
6 csbopg 
 |-  ( b e. _V -> [_ b / y ]_ <. a , y >. = <. [_ b / y ]_ a , [_ b / y ]_ y >. )
7 6 elv 
 |-  [_ b / y ]_ <. a , y >. = <. [_ b / y ]_ a , [_ b / y ]_ y >.
8 vex 
 |-  b e. _V
9 8 csbconstgi 
 |-  [_ b / y ]_ a = a
10 8 csbvargi 
 |-  [_ b / y ]_ y = b
11 9 10 opeq12i 
 |-  <. [_ b / y ]_ a , [_ b / y ]_ y >. = <. a , b >.
12 7 11 eqtri 
 |-  [_ b / y ]_ <. a , y >. = <. a , b >.
13 dfsbcq 
 |-  ( [_ b / y ]_ <. a , y >. = <. a , b >. -> ( [. [_ b / y ]_ <. a , y >. / z ]. ph <-> [. <. a , b >. / z ]. ph ) )
14 12 13 ax-mp 
 |-  ( [. [_ b / y ]_ <. a , y >. / z ]. ph <-> [. <. a , b >. / z ]. ph )
15 3 5 14 3bitri 
 |-  ( [. b / y ]. [. a / x ]. ps <-> [. <. a , b >. / z ]. ph )