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

Theorem eldif 3617
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 3243 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3243 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 480 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2718 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2718 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
65notbid 307 . . . 4 (𝑥 = 𝐴 → (¬ 𝑥𝐶 ↔ ¬ 𝐴𝐶))
74, 6anbi12d 747 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
8 df-dif 3610 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝑥𝐶)}
97, 8elab2g 3385 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
101, 3, 9pm5.21nii 367 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383   = wceq 1523  wcel 2030  Vcvv 3231  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610
This theorem is referenced by:  eldifd  3618  eldifad  3619  eldifbd  3620  difeqri  3763  eldifi  3765  eldifn  3766  neldif  3768  difdif  3769  ddif  3775  ssconb  3776  sscon  3777  ssdif  3778  raldifb  3783  elsymdif  3882  symdif2  3885  dfss4  3891  dfun2  3892  dfin2  3893  difin  3894  indifdir  3916  undif3  3921  undif3OLD  3922  difin2  3923  dfnul2  3950  ssdif0  3975  difin0ss  3979  inssdif0  3980  reldisj  4053  disj3  4054  undif4  4068  pssnel  4072  inundif  4079  ssundif  4085  eldifpr  4237  elpwunsn  4256  eldiftp  4260  eldifsn  4350  difprsnss  4361  iundif2  4619  iindif2  4621  disjss3  4684  brdif  4738  difopab  5286  intirr  5549  cnvdif  5574  difxp  5593  xpdifid  5597  wfi  5751  ordunidif  5811  onmindif  5853  imadif  6011  dffv2  6310  eldifpw  7018  ressuppssdif  7361  extmptsuppeq  7364  suppss  7370  suppssr  7371  suppss2  7374  ondif2  7627  oelim2  7720  boxcutc  7993  brsdom  8020  brsdom2  8125  php3  8187  unblem1  8253  unfilem1  8265  elfi2  8361  dfsup2  8391  ordtypelem7  8470  kmlem4  9013  ackbij1lem18  9097  infpssr  9168  isf34lem4  9237  fin17  9254  fin67  9255  dffin7-2  9258  fin1a2lem6  9265  axcclem  9317  pwfseqlem3  9520  grothprim  9694  xrlenlt  10141  nzadd  11463  irradd  11850  irrmul  11851  difreicc  12342  modirr  12781  hashinf  13162  sumss  14499  fsumss  14500  prodss  14721  fprodss  14722  fprodn0f  14766  rpnnen2lem12  14998  dvdsaddre2b  15076  sumeven  15157  bitscmp  15207  lcmfunsnlem2  15400  iserodd  15587  prmodvdslcmf  15798  symgfix2  17882  pmtrdifellem4  17945  sylow2alem2  18079  efgsfo  18198  gsumval3  18354  gsum2dlem1  18415  gsum2dlem2  18416  ablfac1eu  18518  gsumdixp  18655  isnirred  18746  isirred2  18747  irredn0  18749  lsppratlem1  19195  lbsextlem2  19207  mplsubrglem  19487  mplcoe1  19513  mplcoe5  19516  opsrtoslem2  19533  xrsmgmdifsgrp  19831  psgnodpm  19982  symgmatr01lem  20507  elcls  20925  isclo  20939  maxlp  20999  restntr  21034  isreg2  21229  cmpcld  21253  hausdiag  21496  txkgen  21503  kqcldsat  21584  ufinffr  21780  fin1aufil  21783  alexsublem  21895  alexsubALTlem3  21900  ptcmplem5  21907  blcld  22357  shftmbl  23352  vitalilem4  23425  vitalilem5  23426  vitali  23427  mbfeqalem  23454  itg1val2  23496  itg10a  23522  itg1ge0a  23523  mbfi1fseqlem4  23530  itg2uba  23555  itg2splitlem  23560  itg2monolem1  23562  itg2cnlem1  23573  itg2cnlem2  23574  itgss  23623  dvtaylp  24169  pserdvlem2  24227  ellogdm  24430  relogbcxp  24568  cxplogb  24569  logbmpt  24571  atandm  24648  atans2  24703  eldmgm  24793  igamgam  24820  igamf  24822  igamcl  24823  lgam1  24835  gam1  24836  wilthlem2  24840  basellem3  24854  fsumvma  24983  dchrelbas2  25007  dchreq  25028  dchrsum  25039  gausslemma2dlem4  25139  dchrisum0fno1  25245  rplogsum  25261  islnopp  25676  frgrncvvdeq  27289  fusgr2wsp2nb  27314  eleigvec  28944  strlem1  29237  strlem5  29242  hstrlem5  29250  difrab2  29465  suppss3  29630  xrdifh  29670  nndiffz1  29676  ordtconnlem1  30098  esumpinfval  30263  eulerpartlems  30550  eulerpartlemgc  30552  eulerpartlemb  30558  eulerpartlemf  30560  eulerpartlemt  30561  eulerpartlemgh  30568  ballotlemodife  30687  ballotth  30727  reprdifc  30833  hgt750lemb  30862  elmrsubrn  31543  mrsubvrs  31545  dftr6  31766  dffr5  31769  frpoind  31865  frind  31868  brsset  32121  dfon3  32124  ellimits  32142  dffun10  32146  elfuns  32147  fullfunfv  32179  dfrecs2  32182  dfrdg4  32183  dfint3  32184  hfext  32415  onsucsuccmpi  32567  bj-rest10b  33167  iundif1  33513  poimirlem2  33541  poimirlem11  33550  poimirlem12  33551  poimirlem18  33557  poimirlem21  33560  poimirlem22  33561  poimirlem30  33569  itg2addnclem  33591  ftc1anclem5  33619  areacirc  33635  fdc  33671  isfldidl  33997  opelvvdif  34164  iswatN  35598  dochsnkrlem1  37075  ellz1  37647  pellexlem4  37713  pellexlem5  37714  pwinfig  38183  elnonrel  38208  clsk3nimkb  38655  ntrclselnel1  38672  ntrneiel2  38701  ntrneik4w  38715  compel  38958  undif3VD  39432  limcrecl  40179  icccncfext  40418  dvmptfprodlem  40477  stoweidlem26  40561  stoweidlem39  40574  stoweidlem52  40587  fourierdlem42  40684  etransclem18  40787  etransclem46  40815  ovolval4lem1  41184  0ringdif  42195  0ring1eq0  42197  lindslinindsimp1  42571  dignn0fr  42720
  Copyright terms: Public domain W3C validator