Theorem sscon 4083

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 3915	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	con3d 152	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴))
3	2	anim2d 613	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴)))
4		eldif 3899	. . 3 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))
5		eldif 3899	. . 3 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐶 ∖ 𝐵) → 𝑥 ∈ (𝐶 ∖ 𝐴)))
7	6	ssrdv 3927	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2114   ∖ cdif 3886   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906

This theorem is referenced by:  sscond  4086  complss  4091  sscon34b  4244  sorpsscmpl  7688  sbthlem1  9025  sbthlem2  9026  cantnfp1lem1  9599  cantnfp1lem3  9601  isf34lem7  10301  isf34lem6  10302  setsres  17148  chnccat  18592  mplsubglem  21977  cctop  22971  clsval2  23015  ntrss  23020  hauscmplem  23371  ptbasin  23542  cfinfil  23858  csdfil  23859  uniioombllem5  25554  kur14lem6  35393  bj-2upln1upl  37331  dvasin  38025  readvrec2  42793  clsk3nimkb  44467  fourierdlem62  46596  caragendifcl  46942