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 ( 𝐴𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐵𝐴 ) )

Proof

Step Hyp Ref Expression
1 dfpss2 ( 𝐴𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐴 = 𝐵 ) )
2 eqss ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) )
3 2 baib ( 𝐴𝐵 → ( 𝐴 = 𝐵𝐵𝐴 ) )
4 3 notbid ( 𝐴𝐵 → ( ¬ 𝐴 = 𝐵 ↔ ¬ 𝐵𝐴 ) )
5 4 pm5.32i ( ( 𝐴𝐵 ∧ ¬ 𝐴 = 𝐵 ) ↔ ( 𝐴𝐵 ∧ ¬ 𝐵𝐴 ) )
6 1 5 bitri ( 𝐴𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐵𝐴 ) )