Theorem sbcel21v

Description: Class substitution into a membership relation. One direction of sbcel2gv that holds for proper classes. (Contributed by NM, 17-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		sbcex	|- ( [. B / x ]. A e. x -> B e. _V )
2		sbcel2gv	|- ( B e. _V -> ( [. B / x ]. A e. x <-> A e. B ) )
3	2	biimpd	|- ( B e. _V -> ( [. B / x ]. A e. x -> A e. B ) )
4	1 3	mpcom	|- ( [. B / x ]. A e. x -> A e. B )