Theorem sscon 4093

Description: Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)

Assertion

Ref	Expression
sscon	⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))

Proof of Theorem sscon

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3928	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	con3d 153	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴))
3	2	anim2d 624	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴)))
4		eldif 3912	. . 3 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))
5		eldif 3912	. . 3 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐶 ∖ 𝐵) → 𝑥 ∈ (𝐶 ∖ 𝐴)))
7	6	ssrdv 3940	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   ∖ cdif 3899   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905  df-ss 3919

This theorem is used by:  sscond  4096  complss  4101  sscon34b  4253  sorpsscmpl  7739  sbthlem1  9089  sbthlem2  9090  cantnfp1lem1  9661  cantnfp1lem3  9663  isf34lem7  10385  isf34lem6  10386  setsres  17276  chnccat  18720  mplsubglem  22219  cctop  23237  clsval2  23281  ntrss  23286  hauscmplem  23637  ptbasin  23809  cfinfil  24125  csdfil  24126  uniioombllem5  25821  kur14lem6  35798  bj-2upln1upl  37776  dvasin  38461  readvrec2  43244  clsk3nimkb  44888  fourierdlem62  47004  caragendifcl  47350