Metamath Proof Explorer

Theorem sbcel1v

Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018) Avoid ax-13 . (Revised by Wolf Lammen, 30-Apr-2023)

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

Proof

Step Hyp Ref Expression
1 sbcex 
 |-  ( [. A / x ]. x e. B -> A e. _V )
2 elex 
 |-  ( A e. B -> A e. _V )
3 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] x e. B <-> [. A / x ]. x e. B ) )
4 eleq1 
 |-  ( y = A -> ( y e. B <-> A e. B ) )
5 clelsb1 
 |-  ( [ y / x ] x e. B <-> y e. B )
6 3 4 5 vtoclbg 
 |-  ( A e. _V -> ( [. A / x ]. x e. B <-> A e. B ) )
7 1 2 6 pm5.21nii 
 |-  ( [. A / x ]. x e. B <-> A e. B )