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 
|- A e. _V
Assertion sbc6 
|- ( [. A / x ]. ph <-> A. x ( x = A -> ph ) )

Proof

Step Hyp Ref Expression
1 sbc6.1 
 |-  A e. _V
2 sbc6g 
 |-  ( A e. _V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )
3 1 2 ax-mp 
 |-  ( [. A / x ]. ph <-> A. x ( x = A -> ph ) )