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 ( ( 𝐴𝐵𝐵𝐶 ) → 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 pssss ( 𝐴𝐵𝐴𝐵 )
2 ssexg ( ( 𝐴𝐵𝐵𝐶 ) → 𝐴 ∈ V )
3 1 2 sylan ( ( 𝐴𝐵𝐵𝐶 ) → 𝐴 ∈ V )