Metamath Proof Explorer

Theorem sbc6g

Description: An equivalence for class substitution. (Contributed by NM, 11-Oct-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Assertion sbc6g 
|- ( A e. V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )

Proof

Step Hyp Ref Expression
1 alexeqg 
 |-  ( A e. V -> ( A. x ( x = A -> ph ) <-> E. x ( x = A /\ ph ) ) )
2 sbc5 
 |-  ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) )
3 1 2 syl6rbbr 
 |-  ( A e. V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )