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 V [˙B / x]˙ A x A B

Proof

Step Hyp Ref Expression
1 eleq2 x = y A x A y
2 eleq2 y = B A y A B
3 1 2 sbcie2g B V [˙B / x]˙ A x A B