Description: Negation of subclass expressed in terms of intersection and proper subclass. (Contributed by NM, 30-Jun-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nssinpss | ⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inss1 | ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 | |
| 2 | 1 | biantrur | ⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) ) |
| 3 | dfss2 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) | |
| 4 | 3 | necon3bbii | ⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) |
| 5 | df-pss | ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) ) | |
| 6 | 2 4 5 | 3bitr4i | ⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ) |