Theorem ssdif 4098

Description: Difference law for subsets. (Contributed by NM, 28-May-1998.)

Assertion

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

Proof of Theorem ssdif

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3929	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 612	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 3913	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 3913	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3941	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920

This theorem is referenced by:  ssdifd  4099  pssnn  9105  php  9143  fin1a2lem13  10334  axcclem  10379  isercolllem3  15602  mvdco  19386  dprdres  19971  dpjidcl  20001  ablfac1eulem  20015  cntzsdrg  20747  lspsnat  21112  lbsextlem2  21126  lbsextlem3  21127  cnsubdrglem  21385  mplmonmul  22003  clsconn  23386  2ndcdisj2  23413  kqdisj  23688  nulmbl2  25505  i1f1  25659  itg11  25660  itg1climres  25683  limcresi  25854  dvreslem  25878  dvres2lem  25879  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  lhop  25989  elqaa  26298  difres  32686  imadifxp  32687  xrge00  33106  elrspunidl  33520  psrmonmul  33726  eulerpartlemmf  34552  eulerpartlemgf  34556  bj-2upln1upl  37269  pibt2  37669  mblfinlem3  37907  mblfinlem4  37908  ismblfin  37909  cnambfre  37916  divrngidl  38276  dvrelog2  42431  dvrelog3  42432  readvrec2  42728  readvrec  42729  dffltz  42989  cantnftermord  43674  omabs2  43686  radcnvrat  44667  fourierdlem62  46523