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

Metamath Proof Explorer

Theorem sbciegf

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypotheses sbciegf.1 ⊢ Ⅎ x ψ
sbciegf.2 ⊢ x = A → φ ↔ ψ
Assertion sbciegf ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sbciegf.1 ⊢ Ⅎ x ψ
2 sbciegf.2 ⊢ x = A → φ ↔ ψ
3 2 ax-gen ⊢ ∀ x x = A → φ ↔ ψ
4 sbciegft ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → [˙A / x]˙ φ ↔ ψ
5 1 3 4 mp3an23 ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ