![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sscon | Structured version Visualization version GIF version |
Description: Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.) |
Ref | Expression |
---|---|
sscon | ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3988 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | con3d 152 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴)) |
3 | 2 | anim2d 612 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))) |
4 | eldif 3972 | . . 3 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)) | |
5 | eldif 3972 | . . 3 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴)) | |
6 | 3, 4, 5 | 3imtr4g 296 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐶 ∖ 𝐵) → 𝑥 ∈ (𝐶 ∖ 𝐴))) |
7 | 6 | ssrdv 4000 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∈ wcel 2105 ∖ cdif 3959 ⊆ wss 3962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-dif 3965 df-ss 3979 |
This theorem is referenced by: sscond 4155 complss 4160 sscon34b 4309 sorpsscmpl 7752 sbthlem1 9121 sbthlem2 9122 cantnfp1lem1 9715 cantnfp1lem3 9717 isf34lem7 10416 isf34lem6 10417 setsres 17211 mplsubglem 22036 cctop 23028 clsval2 23073 ntrss 23078 hauscmplem 23429 ptbasin 23600 cfinfil 23916 csdfil 23917 uniioombllem5 25635 kur14lem6 35195 bj-2upln1upl 37006 dvasin 37690 readvrec2 42369 readvrec 42370 clsk3nimkb 44029 fourierdlem62 46123 caragendifcl 46469 |
Copyright terms: Public domain | W3C validator |