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	⊢ ( [ 𝐵 / 𝑥 ] 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐵 / 𝑥 ] 𝐴 ∈ 𝑥 → 𝐵 ∈ V )
2		sbcel2gv	⊢ ( 𝐵 ∈ V → ( [ 𝐵 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) )
3	2	biimpd	⊢ ( 𝐵 ∈ V → ( [ 𝐵 / 𝑥 ] 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝐵 ) )
4	1 3	mpcom	⊢ ( [ 𝐵 / 𝑥 ] 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝐵 )