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

Proof

Step Hyp Ref Expression
1 sbcop.z ⊢ z = x y → φ ↔ ψ
2 sbc5 ⊢ [˙a / x]˙ ψ ↔ ∃ x x = a ∧ ψ
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 → ψ → φ
7 5 6 biimtrdi ⊢ x = a → z = a y → ψ → φ
8 7 com23 ⊢ x = a → ψ → z = a y → φ
9 8 imp ⊢ x = a ∧ ψ → z = a y → φ
10 9 exlimiv ⊢ ∃ x x = a ∧ ψ → z = a y → φ
11 2 10 sylbi ⊢ [˙a / x]˙ ψ → z = a y → φ
12 11 alrimiv ⊢ [˙a / x]˙ ψ → ∀ z z = a y → φ
13 opex ⊢ a y ∈ V
14 13 sbc6 ⊢ [˙ a y / z]˙ φ ↔ ∀ z z = a y → φ
15 12 14 sylibr ⊢ [˙a / x]˙ ψ → [˙ a y / z]˙ φ
16 sbc5 ⊢ [˙ a y / z]˙ φ ↔ ∃ z z = a y ∧ φ
17 1 biimpd ⊢ z = x y → φ → ψ
18 5 17 biimtrdi ⊢ x = a → z = a y → φ → ψ
19 18 com3l ⊢ z = a y → φ → x = a → ψ
20 19 imp ⊢ z = a y ∧ φ → x = a → ψ
21 20 alrimiv ⊢ z = a y ∧ φ → ∀ x x = a → ψ
22 vex ⊢ a ∈ V
23 22 sbc6 ⊢ [˙a / x]˙ ψ ↔ ∀ x x = a → ψ
24 21 23 sylibr ⊢ z = a y ∧ φ → [˙a / x]˙ ψ
25 24 exlimiv ⊢ ∃ z z = a y ∧ φ → [˙a / x]˙ ψ
26 16 25 sylbi ⊢ [˙ a y / z]˙ φ → [˙a / x]˙ ψ
27 15 26 impbii ⊢ [˙a / x]˙ ψ ↔ [˙ a y / z]˙ φ