Metamath Proof Explorer

Theorem dfpss3

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 dfpss2 
 |-  ( A C. B <-> ( A C_ B /\ -. A = B ) )
2 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
3 2 baib 
 |-  ( A C_ B -> ( A = B <-> B C_ A ) )
4 3 notbid 
 |-  ( A C_ B -> ( -. A = B <-> -. B C_ A ) )
5 4 pm5.32i 
 |-  ( ( A C_ B /\ -. A = B ) <-> ( A C_ B /\ -. B C_ A ) )
6 1 5 bitri 
 |-  ( A C. B <-> ( A C_ B /\ -. B C_ A ) )