Theorem ssdif 4119

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 3952	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 611	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 3936	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 3936	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3964	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2108   ∖ cdif 3923   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943

This theorem is referenced by:  ssdifd  4120  pssnn  9182  php  9221  phpOLD  9231  fin1a2lem13  10426  axcclem  10471  isercolllem3  15683  mvdco  19426  dprdres  20011  dpjidcl  20041  ablfac1eulem  20055  cntzsdrg  20762  lspsnat  21106  lbsextlem2  21120  lbsextlem3  21121  cnsubdrglem  21386  mplmonmul  21994  clsconn  23368  2ndcdisj2  23395  kqdisj  23670  nulmbl2  25489  i1f1  25643  itg11  25644  itg1climres  25667  limcresi  25838  dvreslem  25862  dvres2lem  25863  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  lhop  25973  elqaa  26282  difres  32581  imadifxp  32582  xrge00  33007  elrspunidl  33443  eulerpartlemmf  34407  eulerpartlemgf  34411  bj-2upln1upl  37042  pibt2  37435  mblfinlem3  37683  mblfinlem4  37684  ismblfin  37685  cnambfre  37692  divrngidl  38052  dvrelog2  42077  dvrelog3  42078  readvrec2  42404  readvrec  42405  dffltz  42657  cantnftermord  43344  omabs2  43356  radcnvrat  44338  fourierdlem62  46197