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

Metamath Proof Explorer

Theorem sbcieg

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005) Avoid ax-10 , ax-12 . (Revised by GG, 12-Oct-2024)

Ref Expression
Hypothesis sbcieg.1 ⊢ x = A → φ ↔ ψ
Assertion sbcieg ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sbcieg.1 ⊢ x = A → φ ↔ ψ
2 df-sbc ⊢ [˙A / x]˙ φ ↔ A ∈ x | φ
3 1 elabg ⊢ A ∈ V → A ∈ x | φ ↔ ψ
4 2 3 bitrid ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ