Metamath Proof Explorer

Theorem sbcel2gv

Description: Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( x = y -> ( A e. x <-> A e. y ) )
2 eleq2 
 |-  ( y = B -> ( A e. y <-> A e. B ) )
3 1 2 sbcie2g 
 |-  ( B e. V -> ( [. B / x ]. A e. x <-> A e. B ) )