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

Theorem eldif 3733
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 3364 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3364 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 466 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2838 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2838 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
65notbid 307 . . . 4 (𝑥 = 𝐴 → (¬ 𝑥𝐶 ↔ ¬ 𝐴𝐶))
74, 6anbi12d 616 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
8 df-dif 3726 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝑥𝐶)}
97, 8elab2g 3504 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
101, 3, 9pm5.21nii 367 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 382   = wceq 1631  wcel 2145  Vcvv 3351  cdif 3720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726
This theorem is referenced by:  eldifd  3734  eldifad  3735  eldifbd  3736  difeqri  3881  eldifi  3883  eldifn  3884  neldif  3886  difdif  3887  ddif  3893  ssconb  3894  sscon  3895  ssdif  3896  raldifb  3901  elsymdif  3998  symdif2  4001  dfss4  4007  dfun2  4008  dfin2  4009  difin  4010  indifdir  4032  undif3  4037  difin2  4038  dfnul2  4065  ssdif0  4089  difin0ss  4093  inssdif0  4094  reldisj  4163  disj3  4164  undif4  4177  pssnel  4181  inundif  4188  ssundif  4194  eldifpr  4343  elpwunsn  4362  eldiftp  4365  eldifsn  4453  difprsnss  4465  iundif2  4721  iindif2  4723  disjss3  4785  brdif  4839  difopab  5392  intirr  5655  cnvdif  5680  difxp  5699  xpdifid  5703  wfi  5856  ordunidif  5916  onmindif  5958  imadif  6113  dffv2  6413  eldifpw  7123  ressuppssdif  7467  extmptsuppeq  7470  suppss  7477  suppssr  7478  suppss2  7481  ondif2  7736  oelim2  7829  boxcutc  8105  brsdom  8132  brsdom2  8240  php3  8302  unblem1  8368  unfilem1  8380  elfi2  8476  dfsup2  8506  ordtypelem7  8585  kmlem4  9177  ackbij1lem18  9261  infpssr  9332  isf34lem4  9401  fin17  9418  fin67  9419  dffin7-2  9422  fin1a2lem6  9429  axcclem  9481  pwfseqlem3  9684  grothprim  9858  xrlenlt  10305  nzadd  11627  irradd  12015  irrmul  12016  difreicc  12511  modirr  12949  hashinf  13326  sumss  14663  fsumss  14664  prodss  14884  fprodss  14885  fprodn0f  14928  rpnnen2lem12  15160  dvdsaddre2b  15238  sumeven  15318  bitscmp  15368  lcmfunsnlem2  15561  iserodd  15747  prmodvdslcmf  15958  symgfix2  18043  pmtrdifellem4  18106  sylow2alem2  18240  efgsfo  18359  gsumval3  18515  gsum2dlem1  18576  gsum2dlem2  18577  ablfac1eu  18680  gsumdixp  18817  isnirred  18908  isirred2  18909  irredn0  18911  lsppratlem1  19362  lbsextlem2  19374  mplsubrglem  19654  mplcoe1  19680  mplcoe5  19683  opsrtoslem2  19700  xrsmgmdifsgrp  19998  psgnodpm  20149  symgmatr01lem  20678  elcls  21098  isclo  21112  maxlp  21172  restntr  21207  isreg2  21402  cmpcld  21426  hausdiag  21669  txkgen  21676  kqcldsat  21757  ufinffr  21953  fin1aufil  21956  alexsublem  22068  alexsubALTlem3  22073  ptcmplem5  22080  blcld  22530  shftmbl  23526  vitalilem4  23599  vitalilem5  23600  vitali  23601  mbfeqalem  23629  itg1val2  23671  itg10a  23697  itg1ge0a  23698  mbfi1fseqlem4  23705  itg2uba  23730  itg2splitlem  23735  itg2monolem1  23737  itg2cnlem1  23748  itg2cnlem2  23749  itgss  23798  dvtaylp  24344  pserdvlem2  24402  ellogdm  24606  relogbcxp  24744  cxplogb  24745  logbmpt  24747  atandm  24824  atans2  24879  eldmgm  24969  igamgam  24996  igamf  24998  igamcl  24999  lgam1  25011  gam1  25012  wilthlem2  25016  basellem3  25030  fsumvma  25159  dchrelbas2  25183  dchreq  25204  dchrsum  25215  gausslemma2dlem4  25315  dchrisum0fno1  25421  rplogsum  25437  islnopp  25852  frgrncvvdeq  27491  fusgr2wsp2nb  27516  eleigvec  29156  strlem1  29449  strlem5  29454  hstrlem5  29462  difrab2  29677  suppss3  29842  xrdifh  29882  nndiffz1  29888  ordtconnlem1  30310  esumpinfval  30475  eulerpartlems  30762  eulerpartlemgc  30764  eulerpartlemb  30770  eulerpartlemf  30772  eulerpartlemt  30773  eulerpartlemgh  30780  ballotlemodife  30899  ballotth  30939  reprdifc  31045  hgt750lemb  31074  elmrsubrn  31755  mrsubvrs  31757  dftr6  31978  dffr5  31981  frpoind  32077  frind  32080  brsset  32333  dfon3  32336  ellimits  32354  dffun10  32358  elfuns  32359  fullfunfv  32391  dfrecs2  32394  dfrdg4  32395  dfint3  32396  hfext  32627  onsucsuccmpi  32779  bj-rest10b  33374  iundif1  33716  poimirlem2  33744  poimirlem11  33753  poimirlem12  33754  poimirlem18  33760  poimirlem21  33763  poimirlem22  33764  poimirlem30  33772  itg2addnclem  33793  ftc1anclem5  33821  areacirc  33837  fdc  33873  isfldidl  34199  opelvvdif  34366  iswatN  35802  dochsnkrlem1  37279  ellz1  37856  pellexlem4  37922  pellexlem5  37923  pwinfig  38392  elnonrel  38417  clsk3nimkb  38864  ntrclselnel1  38881  ntrneiel2  38910  ntrneik4w  38924  compel  39167  undif3VD  39640  limcrecl  40379  icccncfext  40618  dvmptfprodlem  40677  stoweidlem26  40760  stoweidlem39  40773  stoweidlem52  40786  fourierdlem42  40883  etransclem18  40986  etransclem46  41014  ovolval4lem1  41383  0ringdif  42398  0ring1eq0  42400  lindslinindsimp1  42774  dignn0fr  42923
  Copyright terms: Public domain W3C validator