Theorem eldif 4048

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.

Step	Hyp	Ref	Expression
1		elex 3471	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3471	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2848	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2848	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 4046	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3633	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ∖ cdif 4044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4046

This theorem is used by:  eldifd  4049  eldifad  4050  eldifbd  4051  elneeldif  4052  velcomp  4053  difeqri  4064  nfdif  4065  eldifi  4066  eldifn  4067  neldif  4069  difdif  4070  ssconb  4077  sscon  4078  ssdif  4079  raldifb  4084  elsymdif  4202  dfss4  4213  dfun2  4214  dfin2  4215  difin  4216  indifdi  4238  undif3  4244  difin2  4245  ssdif0  4313  difin0ss  4320  inssdif0OLD  4322  reldisj  4405  disj3  4406  undif4  4419  pssnel  4423  inundif  4434  ssundif  4442  eldifpr  4615  elpwunsn  4641  eldiftp  4644  eldifsn  4744  difprsnss  4758  iundif2  5031  iindif1  5034  iindif2  5036  disjss3  5101  brdif  5157  dffr6  5607  difopab  5809  intirr  6114  cnvdif  6136  difxp  6157  xpdifid  6161  xpdifcnvepel  6162  frpoind  6348  ordunidif  6416  onmindif  6460  imadif  6629  dffv2  6985  eldifpw  7786  releldmdifi  8061  funeldmdif  8064  xpord2pred  8169  xpord2indlem  8171  ressuppssdif  8210  extmptsuppeq  8213  suppss  8219  suppssr  8220  suppssrg  8221  suppss2  8225  suppofssd  8228  suppcoss  8232  ondif2  8518  oelim2  8612  eldifsucnn  8681  boxcutc  8977  brsdom  9009  brsdom2  9128  php3  9232  unblem1  9292  unfilem1  9305  elfi2  9413  dfsup2  9443  ordtypelem7  9525  ssttrcl  9723  ttrcltr  9724  dmttrcl  9729  frind  9761  kmlem4  10239  ackbij1lem18  10321  infpssr  10393  isf34lem4  10462  fin17  10479  fin67  10480  dffin7-2  10483  fin1a2lem6  10490  axcclem  10542  pwfseqlem3  10752  grothprim  10926  xrlenlt  11381  nzadd  12751  irradd  13108  irrmul  13109  difreicc  13622  fzdif1  13746  modirr  14092  hashinf  14486  sumss  15899  fsumss  15900  prodss  16123  fprodss  16124  fprodn0f  16167  rpnnen2lem12  16402  dvdsaddre2b  16486  sumeven  16566  bitscmp  16617  lcmfunsnlem2  16824  iserodd  17022  prmodvdslcmf  17234  chnccat  18809  symgfix2  19639  pmtrdifellem4  19702  sylow2alem2  19841  efgsfo  19962  gsumval3  20130  gsum2dlem1  20193  gsum2dlem2  20194  ablfac1eu  20298  gsumdixp  20557  isnirred  20659  isirred2  20660  irredn0  20662  0ringdif  20787  0ring1eq0  20794  isdrng3lem2  21015  lsppratlem1  21434  lbsextlem2  21446  xrsmgmdifsgrp  21724  psgnodpm  21903  mplsubrglem  22320  mplcoe1  22355  mplcoe5  22358  opsrtoslem2  22374  selvcllem5  22457  selvvvval  22460  symgmatr01lem  22977  elcls  23400  isclo  23414  maxlp  23474  restntr  23509  isreg2  23704  cmpcld  23729  hausdiag  23973  txkgen  23980  kqcldsat  24061  ufinffr  24257  fin1aufil  24260  alexsublem  24372  alexsubALTlem3  24377  ptcmplem5  24384  blcld  24833  shftmbl  25868  vitalilem4  25941  vitalilem5  25942  vitali  25943  mbfeqalem1  25971  itg1val2  26014  itg10a  26040  itg1ge0a  26041  mbfi1fseqlem4  26048  itg2uba  26073  itg2splitlem  26078  itg2monolem1  26080  itg2cnlem1  26091  itg2cnlem2  26092  itgss  26141  dvtaylp  26706  pserdvlem2  26764  ellogdm  26976  relogbcxp  27122  cxplogb  27123  logbmpt  27125  atandm  27213  atans2  27268  eldmgm  27358  igamgam  27385  igamf  27387  igamcl  27388  lgam1  27400  gam1  27401  wilthlem2  27405  basellem3  27419  fsumvma  27549  dchrelbas2  27573  dchreq  27594  dchrsum  27605  gausslemma2dlem4  27705  2sqreultblem  27784  dchrisum0fno1  27847  rplogsum  27863  newbday  28297  ltslpss  28303  islnopp  29224  frgrncvvdeq  30919  fusgr2wsp2nb  30944  eleigvec  32568  strlem1  32861  strlem5  32866  hstrlem5  32874  difrab2  33145  nfpconfp  33277  fdifsupp  33329  suppiniseg  33330  suppss3  33365  fsuppcurry1  33366  fsuppcurry2  33367  xrdifh  33422  nndiffz1  33428  elrgspnsubrunlem2  33859  ist0cld  34515  ordtconnlem1  34606  esumpinfval  34755  eulerpartlems  35042  eulerpartlemgc  35044  eulerpartlemb  35050  eulerpartlemf  35052  eulerpartlemt  35053  eulerpartlemgh  35060  ballotlemodife  35180  ballotth  35220  reprdifc  35306  hgt750lemb  35335  onvf1od  35986  elmrsubrn  36403  mrsubvrs  36405  dftr6  36640  brsset  36775  dfon3  36778  ellimits  36796  dffun10  36800  elfuns  36801  fullfunfv  36835  dfrecs2  36838  dfrdg4  36839  dfint3  36840  hfext  37058  onsucsuccmpi  37355  bj-rest10b  38146  difunieq  38434  pibt2  38477  iundif1  38659  lindsadd  38673  poimirlem2  38677  poimirlem11  38686  poimirlem12  38687  poimirlem18  38693  poimirlem21  38696  poimirlem22  38697  poimirlem30  38705  itg2addnclem  38726  ftc1anclem5  38752  areacirc  38768  fdc  38816  isfldidl  39139  opelvvdif  39333  iswatN  41188  dochsnkrlem1  42663  unitscyglem4  43385  redvmptabs  43548  fsuppssindlem1  43756  ellz1  43915  pellexlem4  43976  pellexlem5  43977  ordeldif  44397  ordeldifsucon  44398  ordeldif1o  44399  cantnfresb  44463  cantnf2  44464  oadif1lem  44518  oadif1  44519  infordmin  44670  minregex  44672  pwinfig  44699  elnonrel  44723  sqrtcvallem1  44768  clsk3nimkb  45177  ntrclselnel1  45194  ntrneiel2  45223  ntrneik4w  45237  undif3VD  46000  iindif2f  46311  limcrecl  46777  icccncfext  47033  dvmptfprodlem  47090  stoweidlem26  47172  stoweidlem39  47185  stoweidlem52  47198  fourierdlem42  47295  etransclem18  47398  etransclem46  47426  ovolval4lem1  47795  requad01  48855  dfnbgr6  49091  lindslinindsimp1  49705  dignn0fr  49849