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

Theorem eldif 3577
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 3207 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3207 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 481 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2687 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2687 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
65notbid 308 . . . 4 (𝑥 = 𝐴 → (¬ 𝑥𝐶 ↔ ¬ 𝐴𝐶))
74, 6anbi12d 746 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
8 df-dif 3570 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝑥𝐶)}
97, 8elab2g 3347 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
101, 3, 9pm5.21nii 368 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 384   = wceq 1481  wcel 1988  Vcvv 3195  cdif 3564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570
This theorem is referenced by:  eldifd  3578  eldifad  3579  eldifbd  3580  difeqri  3722  eldifi  3724  eldifn  3725  neldif  3727  difdif  3728  ddif  3734  ssconb  3735  sscon  3736  ssdif  3737  raldifb  3742  elsymdif  3841  symdif2  3844  dfss4  3850  dfun2  3851  dfin2  3852  difin  3853  indifdir  3875  undif3  3880  undif3OLD  3881  difin2  3882  dfnul2  3909  ssdif0  3933  difin0ss  3937  inssdif0  3938  reldisj  4011  disj3  4012  undif4  4026  pssnel  4030  inundif  4037  ssundif  4043  eldifpr  4195  elpwunsn  4215  eldiftp  4219  eldifsn  4308  difprsnss  4320  iundif2  4578  iindif2  4580  disjss3  4643  brdif  4696  difopab  5242  intirr  5502  cnvdif  5527  difxp  5546  xpdifid  5550  wfi  5701  ordunidif  5761  onmindif  5803  imadif  5961  dffv2  6258  eldifpw  6961  ressuppssdif  7301  extmptsuppeq  7304  suppss  7310  suppssr  7311  suppss2  7314  ondif2  7567  oelim2  7660  boxcutc  7936  brsdom  7963  brsdom2  8069  php3  8131  unblem1  8197  unfilem1  8209  elfi2  8305  dfsup2  8335  ordtypelem7  8414  kmlem4  8960  ackbij1lem18  9044  infpssr  9115  isf34lem4  9184  fin17  9201  fin67  9202  dffin7-2  9205  fin1a2lem6  9212  axcclem  9264  pwfseqlem3  9467  grothprim  9641  xrlenlt  10088  nzadd  11410  irradd  11797  irrmul  11798  difreicc  12289  modirr  12724  hashinf  13105  sumss  14436  fsumss  14437  prodss  14658  fprodss  14659  fprodn0f  14703  rpnnen2lem12  14935  dvdsaddre2b  15010  sumeven  15091  bitscmp  15141  lcmfunsnlem2  15334  iserodd  15521  prmodvdslcmf  15732  symgfix2  17817  pmtrdifellem4  17880  sylow2alem2  18014  efgsfo  18133  gsumval3  18289  gsum2dlem1  18350  gsum2dlem2  18351  ablfac1eu  18453  gsumdixp  18590  isnirred  18681  isirred2  18682  irredn0  18684  lsppratlem1  19128  lbsextlem2  19140  mplsubrglem  19420  mplcoe1  19446  mplcoe5  19449  opsrtoslem2  19466  xrsmgmdifsgrp  19764  psgnodpm  19915  symgmatr01lem  20440  elcls  20858  isclo  20872  maxlp  20932  restntr  20967  isreg2  21162  cmpcld  21186  hausdiag  21429  txkgen  21436  kqcldsat  21517  ufinffr  21714  fin1aufil  21717  alexsublem  21829  alexsubALTlem3  21834  ptcmplem5  21841  blcld  22291  shftmbl  23287  vitalilem4  23361  vitalilem5  23362  vitali  23363  mbfeqalem  23390  itg1val2  23432  itg10a  23458  itg1ge0a  23459  mbfi1fseqlem4  23466  itg2uba  23491  itg2splitlem  23496  itg2monolem1  23498  itg2cnlem1  23509  itg2cnlem2  23510  itgss  23559  dvtaylp  24105  pserdvlem2  24163  ellogdm  24366  relogbcxp  24504  cxplogb  24505  logbmpt  24507  atandm  24584  atans2  24639  eldmgm  24729  igamgam  24756  igamf  24758  igamcl  24759  lgam1  24771  gam1  24772  wilthlem2  24776  basellem3  24790  fsumvma  24919  dchrelbas2  24943  dchreq  24964  dchrsum  24975  gausslemma2dlem4  25075  dchrisum0fno1  25181  rplogsum  25197  islnopp  25612  frgrncvvdeq  27153  fusgr2wsp2nb  27172  eleigvec  28786  strlem1  29079  strlem5  29084  hstrlem5  29092  difrab2  29311  suppss3  29476  xrdifh  29516  nndiffz1  29522  ordtconnlem1  29944  esumpinfval  30109  eulerpartlems  30396  eulerpartlemgc  30398  eulerpartlemb  30404  eulerpartlemf  30406  eulerpartlemt  30407  eulerpartlemgh  30414  ballotlemodife  30533  ballotth  30573  reprdifc  30679  hgt750lemb  30708  elmrsubrn  31391  mrsubvrs  31393  dftr6  31615  dffr5  31618  frind  31714  brsset  31971  dfon3  31974  ellimits  31992  dffun10  31996  elfuns  31997  fullfunfv  32029  dfrecs2  32032  dfrdg4  32033  dfint3  32034  hfext  32265  onsucsuccmpi  32417  bj-rest10b  33017  iundif1  33354  poimirlem2  33382  poimirlem11  33391  poimirlem12  33392  poimirlem18  33398  poimirlem21  33401  poimirlem22  33402  poimirlem30  33410  itg2addnclem  33432  ftc1anclem5  33460  areacirc  33476  fdc  33512  isfldidl  33838  iswatN  35099  dochsnkrlem1  36577  ellz1  37149  pellexlem4  37215  pellexlem5  37216  pwinfig  37685  elnonrel  37710  clsk3nimkb  38158  ntrclselnel1  38175  ntrneiel2  38204  ntrneik4w  38218  compel  38461  undif3VD  38938  limcrecl  39661  icccncfext  39863  dvmptfprodlem  39922  stoweidlem26  40006  stoweidlem39  40019  stoweidlem52  40032  fourierdlem42  40129  etransclem18  40232  etransclem46  40260  ovolval4lem1  40626  0ringdif  41635  0ring1eq0  41637  lindslinindsimp1  42011  dignn0fr  42160
  Copyright terms: Public domain W3C validator