Metamath Proof Explorer


Theorem pssexg

Description: The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022)

Ref Expression
Assertion pssexg ⊢ A ⊂ B ∧ B ∈ C → A ∈ V

Proof

Step Hyp Ref Expression
1 pssss ⊢ A ⊂ B → A ⊆ B
2 ssexg ⊢ A ⊆ B ∧ B ∈ C → A ∈ V
3 1 2 sylan ⊢ A ⊂ B ∧ B ∈ C → A ∈ V