Theorem ssdif 4080

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 3902	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 623	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 4049	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 4049	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3914	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-dif 4047

This theorem is used by:  ssdifd  4081  pssnn  9188  php  9226  fin1a2lem13  10494  axcclem  10539  isercolllem3  15840  mvdco  19665  dprdres  20250  dpjidcl  20280  ablfac1eulem  20294  cntzsdrg  21065  lspsnat  21429  lbsextlem2  21443  lbsextlem3  21444  cnsubdrglem  21730  mplmonmul  22351  clsconn  23754  2ndcdisj2  23782  kqdisj  24057  nulmbl2  25863  i1f1  26017  itg11  26018  itg1climres  26041  limcresi  26211  dvreslem  26235  dvres2lem  26236  dvaddbr  26264  dvmulbr  26265  lhop  26342  elqaa  26651  difres  33242  imadifxp  33243  xrge00  33622  elrspunidl  34025  psrmonmul  34229  eulerpartlemmf  35054  eulerpartlemgf  35058  bj-2upln1upl  38030  pibt2  38434  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  cnambfre  38680  divrngidl  39056  dvrelog2  43208  dvrelog3  43209  readvrec2  43506  readvrec  43507  dffltz  43764  cantnftermord  44416  omabs2  44428  radcnvrat  45392  fourierdlem62  47272