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