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

Theorem eldif 3773
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 3402 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3402 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 468 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2869 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2869 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
65notbid 309 . . . 4 (𝑥 = 𝐴 → (¬ 𝑥𝐶 ↔ ¬ 𝐴𝐶))
74, 6anbi12d 618 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
8 df-dif 3766 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝑥𝐶)}
97, 8elab2g 3544 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
101, 3, 9pm5.21nii 369 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wa 384   = wceq 1637  wcel 2155  Vcvv 3387  cdif 3760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-dif 3766
This theorem is referenced by:  eldifd  3774  eldifad  3775  eldifbd  3776  difeqri  3923  eldifi  3925  eldifn  3926  neldif  3928  difdif  3929  ddif  3935  ssconb  3936  sscon  3937  ssdif  3938  raldifb  3943  elsymdif  4041  symdif2OLD  4049  dfss4  4054  dfun2  4055  dfin2  4056  difin  4057  indifdir  4079  undif3  4084  difin2  4085  dfnul2  4112  ssdif0  4137  difin0ss  4141  inssdif0  4142  reldisj  4211  disj3  4212  undif4  4225  pssnel  4229  inundif  4236  ssundif  4242  eldifpr  4392  elpwunsn  4411  eldiftp  4414  eldifsn  4502  difprsnss  4514  iundif2  4772  iindif2  4774  disjss3  4836  brdif  4890  difopab  5449  intirr  5719  cnvdif  5744  difxp  5763  xpdifid  5767  wfi  5920  ordunidif  5980  onmindif  6022  imadif  6178  dffv2  6486  eldifpw  7200  ressuppssdif  7544  extmptsuppeq  7547  suppss  7554  suppssr  7555  suppss2  7558  ondif2  7813  oelim2  7906  boxcutc  8182  brsdom  8209  brsdom2  8317  php3  8379  unblem1  8445  unfilem1  8457  elfi2  8553  dfsup2  8583  ordtypelem7  8662  kmlem4  9254  ackbij1lem18  9338  infpssr  9409  isf34lem4  9478  fin17  9495  fin67  9496  dffin7-2  9499  fin1a2lem6  9506  axcclem  9558  pwfseqlem3  9761  grothprim  9935  xrlenlt  10382  nzadd  11685  irradd  12025  irrmul  12026  difreicc  12521  modirr  12959  hashinf  13336  sumss  14672  fsumss  14673  prodss  14892  fprodss  14893  fprodn0f  14936  rpnnen2lem12  15168  dvdsaddre2b  15246  sumeven  15324  bitscmp  15373  lcmfunsnlem2  15566  iserodd  15751  prmodvdslcmf  15962  symgfix2  18031  pmtrdifellem4  18094  sylow2alem2  18228  efgsfo  18347  gsumval3  18503  gsum2dlem1  18564  gsum2dlem2  18565  ablfac1eu  18668  gsumdixp  18805  isnirred  18896  isirred2  18897  irredn0  18899  lsppratlem1  19350  lbsextlem2  19362  mplsubrglem  19642  mplcoe1  19668  mplcoe5  19671  opsrtoslem2  19687  xrsmgmdifsgrp  19985  psgnodpm  20135  symgmatr01lem  20665  elcls  21085  isclo  21099  maxlp  21159  restntr  21194  isreg2  21389  cmpcld  21413  hausdiag  21656  txkgen  21663  kqcldsat  21744  ufinffr  21940  fin1aufil  21943  alexsublem  22055  alexsubALTlem3  22060  ptcmplem5  22067  blcld  22517  shftmbl  23513  vitalilem4  23586  vitalilem5  23587  vitali  23588  mbfeqalem1  23616  itg1val2  23659  itg10a  23685  itg1ge0a  23686  mbfi1fseqlem4  23693  itg2uba  23718  itg2splitlem  23723  itg2monolem1  23725  itg2cnlem1  23736  itg2cnlem2  23737  itgss  23786  dvtaylp  24332  pserdvlem2  24390  ellogdm  24593  relogbcxp  24731  cxplogb  24732  logbmpt  24734  atandm  24811  atans2  24866  eldmgm  24956  igamgam  24983  igamf  24985  igamcl  24986  lgam1  24998  gam1  24999  wilthlem2  25003  basellem3  25017  fsumvma  25146  dchrelbas2  25170  dchreq  25191  dchrsum  25202  gausslemma2dlem4  25302  dchrisum0fno1  25408  rplogsum  25424  islnopp  25839  frgrncvvdeq  27478  fusgr2wsp2nb  27503  eleigvec  29138  strlem1  29431  strlem5  29436  hstrlem5  29444  difrab2  29658  suppss3  29823  xrdifh  29863  nndiffz1  29869  ordtconnlem1  30289  esumpinfval  30454  eulerpartlems  30741  eulerpartlemgc  30743  eulerpartlemb  30749  eulerpartlemf  30751  eulerpartlemt  30752  eulerpartlemgh  30759  ballotlemodife  30878  ballotth  30918  reprdifc  31024  hgt750lemb  31053  elmrsubrn  31734  mrsubvrs  31736  dftr6  31956  dffr5  31959  frpoind  32055  frind  32058  brsset  32311  dfon3  32314  ellimits  32332  dffun10  32336  elfuns  32337  fullfunfv  32369  dfrecs2  32372  dfrdg4  32373  dfint3  32374  hfext  32605  onsucsuccmpi  32753  bj-rest10b  33347  iundif1  33690  poimirlem2  33718  poimirlem11  33727  poimirlem12  33728  poimirlem18  33734  poimirlem21  33737  poimirlem22  33738  poimirlem30  33746  itg2addnclem  33767  ftc1anclem5  33795  areacirc  33811  fdc  33846  isfldidl  34172  opelvvdif  34335  iswatN  35768  dochsnkrlem1  37244  ellz1  37826  pellexlem4  37892  pellexlem5  37893  pwinfig  38360  elnonrel  38385  clsk3nimkb  38832  ntrclselnel1  38849  ntrneiel2  38878  ntrneik4w  38892  compel  39134  undif3VD  39606  limcrecl  40335  icccncfext  40574  dvmptfprodlem  40633  stoweidlem26  40716  stoweidlem39  40729  stoweidlem52  40742  fourierdlem42  40839  etransclem18  40942  etransclem46  40970  ovolval4lem1  41339  0ringdif  42432  0ring1eq0  42434  lindslinindsimp1  42808  dignn0fr  42957
  Copyright terms: Public domain W3C validator