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

Metamath Proof Explorer

Theorem sbcie

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004)

Ref Expression
Hypotheses sbcie.1 ⊢ 𝐴 ∈ V
sbcie.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion sbcie ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )

Proof

Step Hyp Ref Expression
1 sbcie.1 ⊢ 𝐴 ∈ V
2 sbcie.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3 2 sbcieg ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
4 1 3 ax-mp ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )