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

Theorem eldif 3266
Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldif  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )

Proof of Theorem eldif
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elex 2900 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2900 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 452 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2440 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2440 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 286 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 692 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3259 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 3020 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 343 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   _Vcvv 2892    \ cdif 3253
This theorem is referenced by:  eldifd  3267  eldifad  3268  eldifbd  3269  difeqri  3403  eldifi  3405  eldifn  3406  neldif  3408  difdif  3409  ddif  3415  ssconb  3416  sscon  3417  ssdif  3418  raldifb  3423  dfss4  3511  dfun2  3512  dfin2  3513  difin  3514  indifdir  3533  undif3  3538  difin2  3539  symdif2  3543  dfnul2  3566  reldisj  3607  disj3  3608  undif4  3620  ssdif0  3622  pssnel  3629  difin0ss  3630  inssdif0  3631  inundif  3642  ssundif  3647  eldifsn  3863  difprsnss  3870  iundif2  4092  iindif2  4094  disjss3  4145  brdif  4194  ordunidif  4563  onmindif  4604  eldifpw  4688  elpwunsn  4690  difopab  4939  intirr  5185  cnvdif  5211  imadif  5461  dffv2  5728  suppss  5795  suppssr  5796  suppss2  6232  difxp  6312  ondif2  6675  oelim2  6767  boxcutc  7034  brsdom  7059  brsdom2  7160  php3  7222  unblem1  7288  unfilem1  7300  elfi2  7347  dfsup2  7375  dfsup2OLD  7376  ordtypelem7  7419  cantnfreslem  7557  kmlem4  7959  ackbij1lem18  8043  infpssr  8114  isf34lem4  8183  fin17  8200  fin67  8201  dffin7-2  8204  fin1a2lem6  8211  axcclem  8263  pwfseqlem3  8461  grothprim  8635  xrlenlt  9069  irradd  10523  irrmul  10524  difreicc  10953  modirr  11206  hashinf  11543  sumss  12438  fsumss  12439  rpnnen2  12745  bitscmp  12870  iserodd  13129  sylow2alem2  15172  efgsfo  15291  gsumval3  15434  gsum2d  15466  ablfac1eu  15551  gsumdixp  15635  isnirred  15725  isirred2  15726  irredn0  15728  lsppratlem1  16139  lbsextlem2  16151  mplsubrglem  16422  mplcoe1  16448  mplcoe2  16450  opsrtoslem2  16465  elcls  17053  isclo  17067  maxlp  17126  restntr  17161  isreg2  17356  cmpcld  17380  hausdiag  17591  txkgen  17598  kqcldsat  17679  ufinffr  17875  fin1aufil  17878  alexsublem  17989  alexsubALTlem3  17994  ptcmplem5  18001  blcld  18418  shftmbl  19293  vitalilem4  19363  vitalilem5  19364  vitali  19365  mbfeqalem  19394  itg1val2  19436  itg10a  19462  itg1ge0a  19463  mbfi1fseqlem4  19470  itg2uba  19495  itg2splitlem  19500  itg2monolem1  19502  itg2cnlem1  19513  itg2cnlem2  19514  itgss  19563  dvtaylp  20146  pserdvlem2  20204  ellogdm  20390  atandm  20576  atans2  20631  wilthlem2  20712  basellem3  20725  fsumvma  20857  dchrelbas2  20881  dchreq  20902  dchrsum  20913  dchrisum0fno1  21065  rplogsum  21081  isusgra0  21236  nbcusgra  21331  eleigvec  23301  strlem1  23594  strlem5  23599  hstrlem5  23607  suppss2f  23885  xrdifh  23972  eldifpr  24181  eldiftp  24182  esumpinfval  24252  ballotlemodife  24527  ballotth  24567  eldmgm  24578  igamgam  24605  igamf  24607  igamcl  24608  lgam1  24620  gam1  24621  prodss  25045  fprodss  25046  dftr6  25124  dffr5  25127  wfi  25224  frind  25260  elsymdif  25384  brsset  25446  dfon3  25449  ellimits  25467  elfuns  25471  fullfunfv  25503  dfrdg4  25506  tfrqfree  25507  hfext  25831  onsucsuccmpi  25900  itg2addnclem  25950  areacirc  25981  fdc  26133  isfldidl  26362  ellz1  26509  pellexlem4  26579  pellexlem5  26580  compel  27302  stoweidlem26  27436  stoweidlem39  27449  stoweidlem52  27462  frgraunss  27741  frgrancvvdeqlem3  27777  frgrancvvdeqlem9  27786  frgrawopreglem3  27791  frgrawopreglem4  27792  frgrawopreg  27794  undif3VD  28328  iswatN  30159  dochsnkrlem1  31635
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-dif 3259
  Copyright terms: Public domain W3C validator