Metamath Proof Explorer


Theorem dfpss2

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996)

Ref Expression
Assertion dfpss2 ABAB¬A=B

Proof

Step Hyp Ref Expression
1 df-pss ABABAB
2 df-ne AB¬A=B
3 2 anbi2i ABABAB¬A=B
4 1 3 bitri ABAB¬A=B