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 → φ ↔ ψ
Assertion sbcop ⊢ [˙b / y]˙ [˙a / x]˙ ψ ↔ [˙ a b / z]˙ φ

Proof

Step Hyp Ref Expression
1 sbcop.z ⊢ z = x y → φ ↔ ψ
2 1 sbcop1 ⊢ [˙a / x]˙ ψ ↔ [˙ a y / z]˙ φ
3 2 sbcbii ⊢ [˙b / y]˙ [˙a / x]˙ ψ ↔ [˙b / y]˙ [˙ a y / z]˙ φ
4 sbcnestgw ⊢ b ∈ V → [˙b / y]˙ [˙ a y / z]˙ φ ↔ [˙⦋ b / y⦌ a y / z]˙ φ
5 4 elv ⊢ [˙b / y]˙ [˙ a y / z]˙ φ ↔ [˙⦋ b / y⦌ a y / z]˙ φ
6 csbopg ⊢ b ∈ 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 ∈ 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]˙ φ ↔ [˙ a b / z]˙ φ
14 12 13 ax-mp ⊢ [˙⦋ b / y⦌ a y / z]˙ φ ↔ [˙ a b / z]˙ φ
15 3 5 14 3bitri ⊢ [˙b / y]˙ [˙a / x]˙ ψ ↔ [˙ a b / z]˙ φ