Metamath Proof Explorer

Theorem dfpss2

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

Ref Expression
Assertion dfpss2 
|- ( A C. B <-> ( A C_ B /\ -. A = B ) )

Proof

Step Hyp Ref Expression
1 df-pss 
 |-  ( A C. B <-> ( A C_ B /\ A =/= B ) )
2 df-ne 
 |-  ( A =/= B <-> -. A = B )
3 2 anbi2i 
 |-  ( ( A C_ B /\ A =/= B ) <-> ( A C_ B /\ -. A = B ) )
4 1 3 bitri 
 |-  ( A C. B <-> ( A C_ B /\ -. A = B ) )