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

Theorem eldif 3893
 Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldif (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))

Proof of Theorem eldif
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3460 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3460 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 484 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2877 . . . 4 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
5 eleq1 2877 . . . . 5 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
65notbid 321 . . . 4 (𝑥 = 𝑦 → (¬ 𝑥𝐶 ↔ ¬ 𝑦𝐶))
74, 6anbi12d 633 . . 3 (𝑥 = 𝑦 → ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ↔ (𝑦𝐵 ∧ ¬ 𝑦𝐶)))
8 eleq1 2877 . . . 4 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
9 eleq1 2877 . . . . 5 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
109notbid 321 . . . 4 (𝑦 = 𝐴 → (¬ 𝑦𝐶 ↔ ¬ 𝐴𝐶))
118, 10anbi12d 633 . . 3 (𝑦 = 𝐴 → ((𝑦𝐵 ∧ ¬ 𝑦𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
12 df-dif 3886 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝑥𝐶)}
137, 11, 12elab2gw 3614 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
141, 3, 13pm5.21nii 383 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3442   ∖ cdif 3880 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-dif 3886 This theorem is referenced by:  eldifd  3894  eldifad  3895  eldifbd  3896  elneeldif  3897  velcomp  3898  difeqri  4055  eldifi  4057  eldifn  4058  neldif  4060  difdif  4061  ddif  4067  ssconb  4068  sscon  4069  ssdif  4070  raldifb  4075  elsymdif  4177  dfss4  4188  dfun2  4189  dfin2  4190  difin  4191  indifdir  4213  undif3  4218  difin2  4219  ssdif0  4280  difin0ss  4285  inssdif0  4286  reldisj  4362  reldisjOLD  4363  disj3  4364  undif4  4377  pssnel  4381  inundif  4388  ssundif  4394  eldifpr  4560  elpwunsn  4584  eldiftp  4587  eldifsn  4683  difprsnss  4695  iundif2  4963  iindif1  4964  iindif2  4966  disjss3  5033  brdif  5087  difopab  5670  intirr  5949  cnvdif  5973  difxp  5992  xpdifid  5996  wfi  6156  ordunidif  6214  onmindif  6255  imadif  6416  dffv2  6743  eldifpw  7483  releldmdifi  7739  funeldmdif  7742  ressuppssdif  7850  extmptsuppeq  7853  suppss  7859  suppssOLD  7860  suppssr  7861  suppssrg  7862  suppss2  7865  suppofssd  7868  suppcoss  7872  ondif2  8128  oelim2  8222  boxcutc  8506  brsdom  8533  brsdom2  8643  php3  8705  unblem1  8772  unfilem1  8784  elfi2  8880  dfsup2  8910  ordtypelem7  8990  kmlem4  9582  ackbij1lem18  9666  infpssr  9737  isf34lem4  9806  fin17  9823  fin67  9824  dffin7-2  9827  fin1a2lem6  9834  axcclem  9886  pwfseqlem3  10089  grothprim  10263  xrlenlt  10713  nzadd  12038  irradd  12380  irrmul  12381  difreicc  12882  modirr  13325  hashinf  13711  sumss  15093  fsumss  15094  prodss  15313  fprodss  15314  fprodn0f  15357  rpnnen2lem12  15590  dvdsaddre2b  15669  sumeven  15748  bitscmp  15797  lcmfunsnlem2  15994  iserodd  16182  prmodvdslcmf  16393  symgfix2  18557  pmtrdifellem4  18620  sylow2alem2  18756  efgsfo  18878  gsumval3  19041  gsum2dlem1  19104  gsum2dlem2  19105  ablfac1eu  19209  gsumdixp  19376  isnirred  19467  isirred2  19468  irredn0  19470  lsppratlem1  19933  lbsextlem2  19945  xrsmgmdifsgrp  20149  psgnodpm  20299  mplsubrglem  20715  mplcoe1  20743  mplcoe5  20746  opsrtoslem2  20762  symgmatr01lem  21299  elcls  21719  isclo  21733  maxlp  21793  restntr  21828  isreg2  22023  cmpcld  22048  hausdiag  22291  txkgen  22298  kqcldsat  22379  ufinffr  22575  fin1aufil  22578  alexsublem  22690  alexsubALTlem3  22695  ptcmplem5  22702  blcld  23153  shftmbl  24183  vitalilem4  24256  vitalilem5  24257  vitali  24258  mbfeqalem1  24286  itg1val2  24329  itg10a  24355  itg1ge0a  24356  mbfi1fseqlem4  24363  itg2uba  24388  itg2splitlem  24393  itg2monolem1  24395  itg2cnlem1  24406  itg2cnlem2  24407  itgss  24456  dvtaylp  25009  pserdvlem2  25067  ellogdm  25274  relogbcxp  25415  cxplogb  25416  logbmpt  25418  atandm  25506  atans2  25561  eldmgm  25651  igamgam  25678  igamf  25680  igamcl  25681  lgam1  25693  gam1  25694  wilthlem2  25698  basellem3  25712  fsumvma  25841  dchrelbas2  25865  dchreq  25886  dchrsum  25897  gausslemma2dlem4  25997  2sqreultblem  26076  dchrisum0fno1  26139  rplogsum  26155  islnopp  26577  frgrncvvdeq  28138  fusgr2wsp2nb  28163  eleigvec  29784  strlem1  30077  strlem5  30082  hstrlem5  30090  difrab2  30312  nfpconfp  30435  suppiniseg  30490  suppss3  30530  fsuppcurry1  30531  fsuppcurry2  30532  xrdifh  30573  nndiffz1  30579  ist0cld  31252  ordtconnlem1  31343  esumpinfval  31508  eulerpartlems  31794  eulerpartlemgc  31796  eulerpartlemb  31802  eulerpartlemf  31804  eulerpartlemt  31805  eulerpartlemgh  31812  ballotlemodife  31931  ballotth  31971  reprdifc  32074  hgt750lemb  32103  elmrsubrn  32946  mrsubvrs  32948  dftr6  33169  dffr5  33172  frpoind  33263  frind  33268  brsset  33610  dfon3  33613  ellimits  33631  dffun10  33635  elfuns  33636  fullfunfv  33668  dfrecs2  33671  dfrdg4  33672  dfint3  33673  hfext  33904  onsucsuccmpi  34051  bj-rest10b  34655  difunieq  34942  pibt2  34985  iundif1  35182  lindsadd  35201  poimirlem2  35210  poimirlem11  35219  poimirlem12  35220  poimirlem18  35226  poimirlem21  35229  poimirlem22  35230  poimirlem30  35238  itg2addnclem  35259  ftc1anclem5  35285  areacirc  35301  fdc  35334  isfldidl  35657  opelvvdif  35831  iswatN  37441  dochsnkrlem1  38916  selvval2lem5  39587  fsuppssindlem1  39625  ellz1  39879  pellexlem4  39944  pellexlem5  39945  infordmin  40411  pwinfig  40431  elnonrel  40456  sqrtcvallem1  40502  clsk3nimkb  40914  ntrclselnel1  40931  ntrneiel2  40960  ntrneik4w  40974  undif3VD  41759  limcrecl  42439  icccncfext  42697  dvmptfprodlem  42754  stoweidlem26  42836  stoweidlem39  42849  stoweidlem52  42862  fourierdlem42  42959  etransclem18  43062  etransclem46  43090  ovolval4lem1  43456  requad01  44307  0ringdif  44662  0ring1eq0  44664  lindslinindsimp1  45032  dignn0fr  45181
 Copyright terms: Public domain W3C validator