Theorem eldif 3899

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 3450	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3450	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2824	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2824	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 318	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 633	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3892	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3623	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ∖ cdif 3886

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892

This theorem is referenced by:  eldifd  3900  eldifad  3901  eldifbd  3902  elneeldif  3903  velcomp  3904  difeqri  4068  nfdif  4069  eldifi  4071  eldifn  4072  neldif  4074  difdif  4075  ssconb  4082  sscon  4083  ssdif  4084  raldifb  4089  elsymdif  4198  dfss4  4209  dfun2  4210  dfin2  4211  difin  4212  indifdi  4234  undif3  4240  difin2  4241  ssdif0  4306  difin0ss  4313  inssdif0  4314  reldisj  4393  disj3  4394  undif4  4407  pssnel  4411  inundif  4419  ssundif  4427  eldifpr  4602  elpwunsn  4628  eldiftp  4631  eldifsn  4731  difprsnss  4744  iundif2  5016  iindif1  5017  iindif2  5019  disjss3  5084  brdif  5138  dffr6  5587  difopab  5786  intirr  6081  cnvdif  6107  difxp  6128  xpdifid  6132  frpoind  6306  ordunidif  6373  onmindif  6417  imadif  6582  dffv2  6935  eldifpw  7722  releldmdifi  7998  funeldmdif  8001  xpord2pred  8095  xpord2indlem  8097  ressuppssdif  8135  extmptsuppeq  8138  suppss  8144  suppssr  8145  suppssrg  8146  suppss2  8150  suppofssd  8153  suppcoss  8157  ondif2  8437  oelim2  8531  eldifsucnn  8600  boxcutc  8889  brsdom  8921  brsdom2  9039  php3  9143  unblem1  9202  unfilem1  9215  elfi2  9327  dfsup2  9357  ordtypelem7  9439  ssttrcl  9636  ttrcltr  9637  dmttrcl  9642  frind  9674  kmlem4  10076  ackbij1lem18  10158  infpssr  10230  isf34lem4  10299  fin17  10316  fin67  10317  dffin7-2  10320  fin1a2lem6  10327  axcclem  10379  pwfseqlem3  10583  grothprim  10757  xrlenlt  11210  nzadd  12575  irradd  12923  irrmul  12924  difreicc  13437  fzdif1  13559  modirr  13904  hashinf  14297  sumss  15686  fsumss  15687  prodss  15912  fprodss  15913  fprodn0f  15956  rpnnen2lem12  16192  dvdsaddre2b  16276  sumeven  16356  bitscmp  16407  lcmfunsnlem2  16609  iserodd  16806  prmodvdslcmf  17018  chnccat  18592  symgfix2  19391  pmtrdifellem4  19454  sylow2alem2  19593  efgsfo  19714  gsumval3  19882  gsum2dlem1  19945  gsum2dlem2  19946  ablfac1eu  20050  gsumdixp  20298  isnirred  20400  isirred2  20401  irredn0  20403  0ringdif  20504  0ring1eq0  20510  lsppratlem1  21145  lbsextlem2  21157  xrsmgmdifsgrp  21389  psgnodpm  21568  mplsubrglem  21982  mplcoe1  22015  mplcoe5  22018  opsrtoslem2  22034  symgmatr01lem  22618  elcls  23038  isclo  23052  maxlp  23112  restntr  23147  isreg2  23342  cmpcld  23367  hausdiag  23610  txkgen  23617  kqcldsat  23698  ufinffr  23894  fin1aufil  23897  alexsublem  24009  alexsubALTlem3  24014  ptcmplem5  24021  blcld  24470  shftmbl  25505  vitalilem4  25578  vitalilem5  25579  vitali  25580  mbfeqalem1  25608  itg1val2  25651  itg10a  25677  itg1ge0a  25678  mbfi1fseqlem4  25685  itg2uba  25710  itg2splitlem  25715  itg2monolem1  25717  itg2cnlem1  25728  itg2cnlem2  25729  itgss  25779  dvtaylp  26335  pserdvlem2  26393  ellogdm  26603  relogbcxp  26749  cxplogb  26750  logbmpt  26752  atandm  26840  atans2  26895  eldmgm  26985  igamgam  27012  igamf  27014  igamcl  27015  lgam1  27027  gam1  27028  wilthlem2  27032  basellem3  27046  fsumvma  27176  dchrelbas2  27200  dchreq  27221  dchrsum  27232  gausslemma2dlem4  27332  2sqreultblem  27411  dchrisum0fno1  27474  rplogsum  27490  newbday  27894  ltslpss  27900  islnopp  28807  frgrncvvdeq  30379  fusgr2wsp2nb  30404  eleigvec  32028  strlem1  32321  strlem5  32326  hstrlem5  32334  difrab2  32567  nfpconfp  32705  fdifsupp  32758  suppiniseg  32759  suppss3  32796  fsuppcurry1  32797  fsuppcurry2  32798  xrdifh  32853  nndiffz1  32859  elrgspnsubrunlem2  33309  ist0cld  33977  ordtconnlem1  34068  esumpinfval  34217  eulerpartlems  34504  eulerpartlemgc  34506  eulerpartlemb  34512  eulerpartlemf  34514  eulerpartlemt  34515  eulerpartlemgh  34522  ballotlemodife  34642  ballotth  34682  reprdifc  34771  hgt750lemb  34800  onvf1od  35289  elmrsubrn  35702  mrsubvrs  35704  dftr6  35933  dffr5  35936  brsset  36069  dfon3  36072  ellimits  36090  dffun10  36094  elfuns  36095  fullfunfv  36129  dfrecs2  36132  dfrdg4  36133  dfint3  36134  hfext  36365  onsucsuccmpi  36625  bj-rest10b  37401  difunieq  37690  pibt2  37733  iundif1  37915  lindsadd  37934  poimirlem2  37943  poimirlem11  37952  poimirlem12  37953  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem30  37971  itg2addnclem  37992  ftc1anclem5  38018  areacirc  38034  fdc  38066  isfldidl  38389  opelvvdif  38585  iswatN  40440  dochsnkrlem1  41915  unitscyglem4  42637  redvmptabs  42792  selvcllem5  43015  selvvvval  43018  fsuppssindlem1  43024  ellz1  43199  pellexlem4  43260  pellexlem5  43261  ordeldif  43686  ordeldifsucon  43687  ordeldif1o  43688  cantnfresb  43752  cantnf2  43753  oadif1lem  43807  oadif1  43808  infordmin  43959  minregex  43961  pwinfig  43988  elnonrel  44012  sqrtcvallem1  44058  clsk3nimkb  44467  ntrclselnel1  44484  ntrneiel2  44513  ntrneik4w  44527  undif3VD  45308  iindif2f  45590  limcrecl  46059  icccncfext  46315  dvmptfprodlem  46372  stoweidlem26  46454  stoweidlem39  46467  stoweidlem52  46480  fourierdlem42  46577  etransclem18  46680  etransclem46  46708  ovolval4lem1  47077  nthrucw  47316  requad01  48097  dfnbgr6  48333  lindslinindsimp1  48933  dignn0fr  49077