MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssdif Structured version   Unicode version

Theorem ssdif 3479
Description: Difference law for subsets. (Contributed by NM, 28-May-1998.)
Assertion
Ref Expression
ssdif  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )

Proof of Theorem ssdif
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ssel 3338 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 559 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  B  /\  -.  x  e.  C ) ) )
3 eldif 3326 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3326 . . 3  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
52, 3, 43imtr4g 270 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A 
\  C )  ->  x  e.  ( B  \  C ) ) )
65ssrdv 3350 1  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1755    \ cdif 3313    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319  df-in 3323  df-ss 3330
This theorem is referenced by:  ssdifd  3480  php  7483  pssnn  7519  mapfienOLD  7915  fin1a2lem13  8569  axcclem  8614  isercolllem3  13128  mvdco  15931  dprdres  16499  dpjidcl  16531  dpjidclOLD  16538  ablfac1eulem  16547  lspsnat  17148  lbsextlem2  17162  lbsextlem3  17163  mplmonmul  17477  cnsubdrglem  17708  clscon  18876  2ndcdisj2  18903  kqdisj  19147  nulmbl2  20860  i1f1  21010  itg11  21011  itg1climres  21034  limcresi  21202  dvreslem  21226  dvres2lem  21227  dvaddbr  21254  dvmulbr  21255  lhop  21330  elqaa  21673  imadifxp  25763  xrge00  25970  eulerpartlemmf  26606  eulerpartlemgf  26610  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  cnambfre  28284  divrngidl  28672  cntzsdrg  29404  bj-2upln1upl  32121
  Copyright terms: Public domain W3C validator