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

Theorem eldif 3471
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 3104 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 3104 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 465 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2515 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2515 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 294 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 710 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3464 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 3234 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 353 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    /\ wa 369    = wceq 1383    e. wcel 1804   _Vcvv 3095    \ cdif 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464
This theorem is referenced by:  eldifd  3472  eldifad  3473  eldifbd  3474  difeqri  3609  eldifi  3611  eldifn  3612  neldif  3614  difdif  3615  ddif  3621  ssconb  3622  sscon  3623  ssdif  3624  raldifb  3629  dfss4  3717  dfun2  3718  dfin2  3719  difin  3720  indifdir  3739  undif3  3744  difin2  3745  symdif2  3749  dfnul2  3772  reldisj  3856  disj3  3857  undif4  3869  ssdif0  3871  pssnel  3879  difin0ss  3880  inssdif0  3881  inundif  3892  ssundif  3897  eldifpr  4031  elpwunsn  4055  eldiftp  4057  eldifsn  4140  difprsnss  4150  iundif2  4382  iindif2  4384  disjss3  4436  brdif  4487  ordunidif  4916  onmindif  4957  difopab  5124  intirr  5375  cnvdif  5402  difxp  5421  xpdifid  5425  imadif  5653  dffv2  5931  suppssOLD  6005  suppssrOLD  6006  suppss2OLD  6515  eldifpw  6597  ressuppssdif  6923  extmptsuppeq  6926  suppss  6932  suppssr  6933  suppss2  6936  ondif2  7154  oelim2  7246  boxcutc  7514  brsdom  7540  brsdom2  7643  php3  7705  unblem1  7774  unfilem1  7786  elfi2  7876  dfsup2  7904  dfsup2OLD  7905  ordtypelem7  7952  kmlem4  8536  ackbij1lem18  8620  infpssr  8691  isf34lem4  8760  fin17  8777  fin67  8778  dffin7-2  8781  fin1a2lem6  8788  axcclem  8840  pwfseqlem3  9041  grothprim  9215  xrlenlt  9655  irradd  11216  irrmul  11217  difreicc  11662  modirr  12038  hashinf  12391  sumss  13527  fsumss  13528  prodss  13735  fprodss  13736  rpnnen2  13940  bitscmp  14069  iserodd  14340  symgfix2  16419  pmtrdifellem4  16482  sylow2alem2  16616  efgsfo  16735  gsumval3OLD  16886  gsumval3  16889  gsum2dlem1  16975  gsum2dlem2  16976  gsum2dOLD  16978  ablfac1eu  17102  gsumdixpOLD  17235  gsumdixp  17236  isnirred  17327  isirred2  17328  irredn0  17330  lsppratlem1  17771  lbsextlem2  17783  mplsubrglem  18078  mplsubrglemOLD  18079  mplcoe1  18105  mplcoe5  18109  mplcoe2OLD  18111  opsrtoslem2  18127  xrsmgmdifsgrp  18433  psgnodpm  18601  symgmatr01lem  19132  elcls  19551  isclo  19565  maxlp  19625  restntr  19660  isreg2  19855  cmpcld  19879  hausdiag  20123  txkgen  20130  kqcldsat  20211  ufinffr  20407  fin1aufil  20410  alexsublem  20521  alexsubALTlem3  20526  ptcmplem5  20533  blcld  20985  shftmbl  21926  vitalilem4  21997  vitalilem5  21998  vitali  21999  mbfeqalem  22026  itg1val2  22068  itg10a  22094  itg1ge0a  22095  mbfi1fseqlem4  22102  itg2uba  22127  itg2splitlem  22132  itg2monolem1  22134  itg2cnlem1  22145  itg2cnlem2  22146  itgss  22195  dvtaylp  22741  pserdvlem2  22799  ellogdm  22996  atandm  23183  atans2  23238  wilthlem2  23319  basellem3  23332  fsumvma  23464  dchrelbas2  23488  dchreq  23509  dchrsum  23520  dchrisum0fno1  23672  rplogsum  23688  islnopp  24089  isusgra0  24323  usgraop  24326  nbcusgra  24439  frgraunss  24971  frgrancvvdeqlem3  25008  frgrancvvdeqlem9  25017  frgrawopreglem3  25022  frgrawopreglem4  25023  frgrawopreg  25025  usg2spot2nb  25041  eleigvec  26852  strlem1  27145  strlem5  27150  hstrlem5  27158  suppss2f  27453  suppss3  27526  xrdifh  27567  nndiffz1  27572  ordtconlem1  27883  esumpinfval  28056  eulerpartlems  28276  eulerpartlemgc  28278  eulerpartlemb  28284  eulerpartlemf  28286  eulerpartlemt  28287  eulerpartlemgh  28294  ballotlemodife  28413  ballotth  28453  eldmgm  28541  igamgam  28568  igamf  28570  igamcl  28571  lgam1  28583  gam1  28584  elmrsubrn  28857  mrsubvrs  28859  dftr6  29154  dffr5  29157  wfi  29262  frind  29298  elsymdif  29448  brsset  29514  dfon3  29517  ellimits  29535  dffun10  29539  elfuns  29540  fullfunfv  29572  dfrdg4  29575  tfrqfree  29576  dfint3  29577  hfext  29815  onsucsuccmpi  29883  iundif1  30012  dvtanlem  30039  itg2addnclem  30041  ftc1anclem5  30069  areacirc  30087  fdc  30213  isfldidl  30440  ellz1  30675  pellexlem4  30743  pellexlem5  30744  compel  31301  limcrecl  31543  icccncfext  31597  stoweidlem26  31697  stoweidlem39  31710  stoweidlem52  31723  fourierdlem42  31820  uhgraedgrnv  32187  lindslinindsimp1  32793  undif3VD  33415  iswatN  35458  dochsnkrlem1  36936  pwinfig  37449
  Copyright terms: Public domain W3C validator