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

Metamath Proof Explorer

Theorem sbc6

Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993) (Proof shortened by Eric Schmidt, 17-Jan-2007)

Ref Expression
Hypothesis sbc6.1 ⊢ 𝐴 ∈ V
Assertion sbc6 ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) )

Proof

Step Hyp Ref Expression
1 sbc6.1 ⊢ 𝐴 ∈ V
2 sbc6g ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
3 1 2 ax-mp ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) )