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 C. B /\ B e. C ) -> A e. _V )

Proof

Step Hyp Ref Expression
1 pssss 
 |-  ( A C. B -> A C_ B )
2 ssexg 
 |-  ( ( A C_ B /\ B e. C ) -> A e. _V )
3 1 2 sylan 
 |-  ( ( A C. B /\ B e. C ) -> A e. _V )