Metamath Proof Explorer

Theorem sbcralg

Description: Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion sbcralg 
|- ( A e. V -> ( [. A / x ]. A. y e. B ph <-> A. y e. B [. A / x ]. ph ) )

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ y A
2 sbcralt 
 |-  ( ( A e. V /\ F/_ y A ) -> ( [. A / x ]. A. y e. B ph <-> A. y e. B [. A / x ]. ph ) )
3 1 2 mpan2 
 |-  ( A e. V -> ( [. A / x ]. A. y e. B ph <-> A. y e. B [. A / x ]. ph ) )