Theorem prcssprc

Description: The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Assertion	prcssprc	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ∉ V ) → 𝐵 ∉ V )

Proof

Step	Hyp	Ref	Expression
1		ssexg	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
2	1	ex	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ∈ V → 𝐴 ∈ V ) )
3	2	nelcon3d	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∉ V → 𝐵 ∉ V ) )
4	3	imp	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ∉ V ) → 𝐵 ∉ V )