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

Theorem eldif 3943
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 3510 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3510 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 481 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2897 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2897 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
65notbid 319 . . . 4 (𝑥 = 𝐴 → (¬ 𝑥𝐶 ↔ ¬ 𝐴𝐶))
74, 6anbi12d 630 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
8 df-dif 3936 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝑥𝐶)}
97, 8elab2g 3665 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
101, 3, 9pm5.21nii 380 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396   = wceq 1528  wcel 2105  Vcvv 3492  cdif 3930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936
This theorem is referenced by:  eldifd  3944  eldifad  3945  eldifbd  3946  elneeldif  3947  velcomp  3948  difeqri  4098  eldifi  4100  eldifn  4101  neldif  4103  difdif  4104  ddif  4110  ssconb  4111  sscon  4112  ssdif  4113  raldifb  4118  elsymdif  4221  dfss4  4232  dfun2  4233  dfin2  4234  difin  4235  indifdir  4257  undif3  4262  difin2  4263  dfnul2OLD  4291  ssdif0  4320  difin0ss  4325  inssdif0  4326  reldisj  4398  disj3  4399  undif4  4412  pssnel  4416  inundif  4423  ssundif  4429  eldifpr  4587  elpwunsn  4613  eldiftp  4616  eldifsn  4711  eldifsnneqOLD  4716  difprsnss  4724  iundif2  4987  iindif1  4988  iindif2  4990  disjss3  5056  brdif  5110  difopab  5695  intirr  5971  cnvdif  5995  difxp  6014  xpdifid  6018  wfi  6174  ordunidif  6232  onmindif  6273  imadif  6431  dffv2  6749  eldifpw  7479  releldmdifi  7733  funeldmdif  7736  ressuppssdif  7840  extmptsuppeq  7843  suppss  7849  suppssr  7850  suppss2  7853  suppofssd  7856  ondif2  8116  oelim2  8210  boxcutc  8493  brsdom  8520  brsdom2  8629  php3  8691  unblem1  8758  unfilem1  8770  elfi2  8866  dfsup2  8896  ordtypelem7  8976  kmlem4  9567  ackbij1lem18  9647  infpssr  9718  isf34lem4  9787  fin17  9804  fin67  9805  dffin7-2  9808  fin1a2lem6  9815  axcclem  9867  pwfseqlem3  10070  grothprim  10244  xrlenlt  10694  nzadd  12018  irradd  12360  irrmul  12361  difreicc  12858  modirr  13298  hashinf  13683  sumss  15069  fsumss  15070  prodss  15289  fprodss  15290  fprodn0f  15333  rpnnen2lem12  15566  dvdsaddre2b  15645  sumeven  15726  bitscmp  15775  lcmfunsnlem2  15972  iserodd  16160  prmodvdslcmf  16371  symgfix2  18473  pmtrdifellem4  18536  sylow2alem2  18672  efgsfo  18794  gsumval3  18956  gsum2dlem1  19019  gsum2dlem2  19020  ablfac1eu  19124  gsumdixp  19288  isnirred  19379  isirred2  19380  irredn0  19382  lsppratlem1  19848  lbsextlem2  19860  mplsubrglem  20147  mplcoe1  20174  mplcoe5  20177  opsrtoslem2  20193  xrsmgmdifsgrp  20510  psgnodpm  20660  symgmatr01lem  21190  elcls  21609  isclo  21623  maxlp  21683  restntr  21718  isreg2  21913  cmpcld  21938  hausdiag  22181  txkgen  22188  kqcldsat  22269  ufinffr  22465  fin1aufil  22468  alexsublem  22580  alexsubALTlem3  22585  ptcmplem5  22592  blcld  23042  shftmbl  24066  vitalilem4  24139  vitalilem5  24140  vitali  24141  mbfeqalem1  24169  itg1val2  24212  itg10a  24238  itg1ge0a  24239  mbfi1fseqlem4  24246  itg2uba  24271  itg2splitlem  24276  itg2monolem1  24278  itg2cnlem1  24289  itg2cnlem2  24290  itgss  24339  dvtaylp  24885  pserdvlem2  24943  ellogdm  25149  relogbcxp  25290  cxplogb  25291  logbmpt  25293  atandm  25381  atans2  25436  eldmgm  25526  igamgam  25553  igamf  25555  igamcl  25556  lgam1  25568  gam1  25569  wilthlem2  25573  basellem3  25587  fsumvma  25716  dchrelbas2  25740  dchreq  25761  dchrsum  25772  gausslemma2dlem4  25872  2sqreultblem  25951  dchrisum0fno1  26014  rplogsum  26030  islnopp  26452  frgrncvvdeq  28015  fusgr2wsp2nb  28040  eleigvec  29661  strlem1  29954  strlem5  29959  hstrlem5  29967  difrab2  30188  nfpconfp  30305  suppss3  30386  fsuppcurry1  30387  fsuppcurry2  30388  xrdifh  30429  nndiffz1  30435  ordtconnlem1  31066  esumpinfval  31231  eulerpartlems  31517  eulerpartlemgc  31519  eulerpartlemb  31525  eulerpartlemf  31527  eulerpartlemt  31528  eulerpartlemgh  31535  ballotlemodife  31654  ballotth  31694  reprdifc  31797  hgt750lemb  31826  elmrsubrn  32664  mrsubvrs  32666  dftr6  32883  dffr5  32886  frpoind  32977  frind  32982  brsset  33247  dfon3  33250  ellimits  33268  dffun10  33272  elfuns  33273  fullfunfv  33305  dfrecs2  33308  dfrdg4  33309  dfint3  33310  hfext  33541  onsucsuccmpi  33688  bj-rest10b  34274  difunieq  34537  pibt2  34580  iundif1  34747  lindsadd  34766  poimirlem2  34775  poimirlem11  34784  poimirlem12  34785  poimirlem18  34791  poimirlem21  34794  poimirlem22  34795  poimirlem30  34803  itg2addnclem  34824  ftc1anclem5  34852  areacirc  34868  fdc  34901  isfldidl  35227  opelvvdif  35401  iswatN  37010  dochsnkrlem1  38485  selvval2lem5  39015  ellz1  39242  pellexlem4  39307  pellexlem5  39308  infordmin  39777  pwinfig  39798  elnonrel  39823  clsk3nimkb  40268  ntrclselnel1  40285  ntrneiel2  40314  ntrneik4w  40328  undif3VD  41093  limcrecl  41786  icccncfext  42046  dvmptfprodlem  42105  stoweidlem26  42188  stoweidlem39  42201  stoweidlem52  42214  fourierdlem42  42311  etransclem18  42414  etransclem46  42442  ovolval4lem1  42808  requad01  43663  0ringdif  44069  0ring1eq0  44071  lindslinindsimp1  44440  dignn0fr  44589
  Copyright terms: Public domain W3C validator