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

Metamath Proof Explorer

Theorem sbciedf

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 29-Dec-2014)

Ref Expression
Hypotheses sbcied.1 ⊢ φ → A ∈ V
sbcied.2 ⊢ φ ∧ x = A → ψ ↔ χ
sbciedf.3 ⊢ Ⅎ x φ
sbciedf.4 ⊢ φ → Ⅎ x χ
Assertion sbciedf ⊢ φ → [˙A / x]˙ ψ ↔ χ

Proof

Step Hyp Ref Expression
1 sbcied.1 ⊢ φ → A ∈ V
2 sbcied.2 ⊢ φ ∧ x = A → ψ ↔ χ
3 sbciedf.3 ⊢ Ⅎ x φ
4 sbciedf.4 ⊢ φ → Ⅎ x χ
5 2 ex ⊢ φ → x = A → ψ ↔ χ
6 3 5 alrimi ⊢ φ → ∀ x x = A → ψ ↔ χ
7 sbciegft ⊢ A ∈ V ∧ Ⅎ x χ ∧ ∀ x x = A → ψ ↔ χ → [˙A / x]˙ ψ ↔ χ
8 1 4 6 7 syl3anc ⊢ φ → [˙A / x]˙ ψ ↔ χ