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=xyφψ
Assertion sbcop [˙b/y]˙[˙a/x]˙ψ[˙ab/z]˙φ

Proof

Step Hyp Ref Expression
1 sbcop.z z=xyφψ
2 1 sbcop1 [˙a/x]˙ψ[˙ay/z]˙φ
3 2 sbcbii [˙b/y]˙[˙a/x]˙ψ[˙b/y]˙[˙ay/z]˙φ
4 sbcnestgw bV[˙b/y]˙[˙ay/z]˙φ[˙b/yay/z]˙φ
5 4 elv [˙b/y]˙[˙ay/z]˙φ[˙b/yay/z]˙φ
6 csbopg bVb/yay=b/yab/yy
7 6 elv b/yay=b/yab/yy
8 vex bV
9 8 csbconstgi b/ya=a
10 8 csbvargi b/yy=b
11 9 10 opeq12i b/yab/yy=ab
12 7 11 eqtri b/yay=ab
13 dfsbcq b/yay=ab[˙b/yay/z]˙φ[˙ab/z]˙φ
14 12 13 ax-mp [˙b/yay/z]˙φ[˙ab/z]˙φ
15 3 5 14 3bitri [˙b/y]˙[˙a/x]˙ψ[˙ab/z]˙φ