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