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

Theorem eldif 3485
Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldif

Proof of Theorem eldif
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3118 . 2
2 elex 3118 . . 3
32adantr 465 . 2
4 eleq1 2529 . . . 4
5 eleq1 2529 . . . . 5
65notbid 294 . . . 4
74, 6anbi12d 710 . . 3
8 df-dif 3478 . . 3
97, 8elab2g 3248 . 2
101, 3, 9pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818   cvv 3109  \cdif 3472
This theorem is referenced by:  eldifd  3486  eldifad  3487  eldifbd  3488  difeqri  3623  eldifi  3625  eldifn  3626  neldif  3628  difdif  3629  ddif  3635  ssconb  3636  sscon  3637  ssdif  3638  raldifb  3643  dfss4  3731  dfun2  3732  dfin2  3733  difin  3734  indifdir  3753  undif3  3758  difin2  3759  symdif2  3763  dfnul2  3786  reldisj  3870  disj3  3871  undif4  3883  ssdif0  3885  pssnel  3893  difin0ss  3894  inssdif0  3895  inundif  3906  ssundif  3911  eldifpr  4046  elpwunsn  4070  eldiftp  4072  eldifsn  4155  difprsnss  4165  iundif2  4397  iindif2  4399  disjss3  4451  brdif  4502  ordunidif  4931  onmindif  4972  difopab  5139  intirr  5390  cnvdif  5417  difxp  5436  xpdifid  5440  imadif  5668  dffv2  5946  suppssOLD  6020  suppssrOLD  6021  suppss2OLD  6530  eldifpw  6612  ressuppssdif  6940  extmptsuppeq  6943  suppss  6949  suppssr  6950  suppss2  6953  ondif2  7171  oelim2  7263  boxcutc  7532  brsdom  7558  brsdom2  7661  php3  7723  unblem1  7792  unfilem1  7804  elfi2  7894  dfsup2  7922  dfsup2OLD  7923  ordtypelem7  7970  kmlem4  8554  ackbij1lem18  8638  infpssr  8709  isf34lem4  8778  fin17  8795  fin67  8796  dffin7-2  8799  fin1a2lem6  8806  axcclem  8858  pwfseqlem3  9059  grothprim  9233  xrlenlt  9673  irradd  11235  irrmul  11236  difreicc  11681  modirr  12057  hashinf  12410  sumss  13546  fsumss  13547  prodss  13754  fprodss  13755  rpnnen2  13959  bitscmp  14088  iserodd  14359  symgfix2  16441  pmtrdifellem4  16504  sylow2alem2  16638  efgsfo  16757  gsumval3OLD  16908  gsumval3  16911  gsum2dlem1  16997  gsum2dlem2  16998  gsum2dOLD  17000  ablfac1eu  17124  gsumdixpOLD  17257  gsumdixp  17258  isnirred  17349  isirred2  17350  irredn0  17352  lsppratlem1  17793  lbsextlem2  17805  mplsubrglem  18100  mplsubrglemOLD  18101  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  opsrtoslem2  18149  xrsmgmdifsgrp  18455  psgnodpm  18624  symgmatr01lem  19155  elcls  19574  isclo  19588  maxlp  19648  restntr  19683  isreg2  19878  cmpcld  19902  hausdiag  20146  txkgen  20153  kqcldsat  20234  ufinffr  20430  fin1aufil  20433  alexsublem  20544  alexsubALTlem3  20549  ptcmplem5  20556  blcld  21008  shftmbl  21949  vitalilem4  22020  vitalilem5  22021  vitali  22022  mbfeqalem  22049  itg1val2  22091  itg10a  22117  itg1ge0a  22118  mbfi1fseqlem4  22125  itg2uba  22150  itg2splitlem  22155  itg2monolem1  22157  itg2cnlem1  22168  itg2cnlem2  22169  itgss  22218  dvtaylp  22765  pserdvlem2  22823  ellogdm  23020  atandm  23207  atans2  23262  wilthlem2  23343  basellem3  23356  fsumvma  23488  dchrelbas2  23512  dchreq  23533  dchrsum  23544  dchrisum0fno1  23696  rplogsum  23712  islnopp  24113  isusgra0  24347  usgraop  24350  nbcusgra  24463  frgraunss  24995  frgrancvvdeqlem3  25032  frgrancvvdeqlem9  25041  frgrawopreglem3  25046  frgrawopreglem4  25047  frgrawopreg  25049  usg2spot2nb  25065  eleigvec  26876  strlem1  27169  strlem5  27174  hstrlem5  27182  suppss2f  27477  suppss3  27550  xrdifh  27591  nndiffz1  27596  ordtconlem1  27906  esumpinfval  28079  eulerpartlems  28299  eulerpartlemgc  28301  eulerpartlemb  28307  eulerpartlemf  28309  eulerpartlemt  28310  eulerpartlemgh  28317  ballotlemodife  28436  ballotth  28476  eldmgm  28564  igamgam  28591  igamf  28593  igamcl  28594  lgam1  28606  gam1  28607  elmrsubrn  28880  mrsubvrs  28882  dftr6  29179  dffr5  29182  wfi  29287  frind  29323  elsymdif  29473  brsset  29539  dfon3  29542  ellimits  29560  dffun10  29564  elfuns  29565  fullfunfv  29597  dfrdg4  29600  tfrqfree  29601  dfint3  29602  hfext  29840  onsucsuccmpi  29908  iundif1  30037  dvtanlem  30064  itg2addnclem  30066  ftc1anclem5  30094  areacirc  30112  fdc  30238  isfldidl  30465  ellz1  30700  pellexlem4  30768  pellexlem5  30769  compel  31347  fprodn0f  31594  limcrecl  31635  icccncfext  31690  dvmptfprodlem  31741  stoweidlem26  31808  stoweidlem39  31821  stoweidlem52  31834  fourierdlem42  31931  etransclem18  32035  etransclem46  32063  uhgraedgrnv  32349  0ringdif  32676  0ring1eq0  32678  lindslinindsimp1  33058  undif3VD  33682  iswatN  35718  dochsnkrlem1  37196  pwinfig  37746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478
  Copyright terms: Public domain W3C validator