Theorem eldif 3924

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ∖ cdif 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917

This theorem is referenced by:  eldifd  3925  eldifad  3926  eldifbd  3927  elneeldif  3928  velcomp  3929  difeqri  4091  nfdif  4092  eldifi  4094  eldifn  4095  neldif  4097  difdif  4098  ddif  4104  ssconb  4105  sscon  4106  ssdif  4107  raldifb  4112  elsymdif  4221  dfss4  4232  dfun2  4233  dfin2  4234  difin  4235  indifdi  4257  undif3  4263  difin2  4264  ssdif0  4329  difin0ss  4336  inssdif0  4337  reldisj  4416  disj3  4417  undif4  4430  pssnel  4434  inundif  4442  ssundif  4451  eldifpr  4622  elpwunsn  4648  eldiftp  4651  eldifsn  4750  difprsnss  4763  iundif2  5038  iindif1  5039  iindif2  5041  disjss3  5106  brdif  5160  dffr6  5594  difopab  5793  difopabOLD  5794  intirr  6091  cnvdif  6116  difxp  6137  xpdifid  6141  frpoind  6315  ordunidif  6382  onmindif  6426  imadif  6600  dffv2  6956  eldifpw  7744  releldmdifi  8024  funeldmdif  8027  xpord2pred  8124  xpord2indlem  8126  ressuppssdif  8164  extmptsuppeq  8167  suppss  8173  suppssr  8174  suppssrg  8175  suppss2  8179  suppofssd  8182  suppcoss  8186  ondif2  8466  oelim2  8559  eldifsucnn  8628  boxcutc  8914  brsdom  8946  brsdom2  9065  php3  9173  unblem1  9239  unfilem1  9254  elfi2  9365  dfsup2  9395  ordtypelem7  9477  ssttrcl  9668  ttrcltr  9669  dmttrcl  9674  frind  9703  kmlem4  10107  ackbij1lem18  10189  infpssr  10261  isf34lem4  10330  fin17  10347  fin67  10348  dffin7-2  10351  fin1a2lem6  10358  axcclem  10410  pwfseqlem3  10613  grothprim  10787  xrlenlt  11239  nzadd  12581  irradd  12932  irrmul  12933  difreicc  13445  fzdif1  13566  modirr  13907  hashinf  14300  sumss  15690  fsumss  15691  prodss  15913  fprodss  15914  fprodn0f  15957  rpnnen2lem12  16193  dvdsaddre2b  16277  sumeven  16357  bitscmp  16408  lcmfunsnlem2  16610  iserodd  16806  prmodvdslcmf  17018  symgfix2  19346  pmtrdifellem4  19409  sylow2alem2  19548  efgsfo  19669  gsumval3  19837  gsum2dlem1  19900  gsum2dlem2  19901  ablfac1eu  20005  gsumdixp  20228  isnirred  20329  isirred2  20330  irredn0  20332  0ringdif  20436  0ring1eq0  20442  lsppratlem1  21057  lbsextlem2  21069  xrsmgmdifsgrp  21320  psgnodpm  21497  mplsubrglem  21913  mplcoe1  21944  mplcoe5  21947  opsrtoslem2  21963  symgmatr01lem  22540  elcls  22960  isclo  22974  maxlp  23034  restntr  23069  isreg2  23264  cmpcld  23289  hausdiag  23532  txkgen  23539  kqcldsat  23620  ufinffr  23816  fin1aufil  23819  alexsublem  23931  alexsubALTlem3  23936  ptcmplem5  23943  blcld  24393  shftmbl  25439  vitalilem4  25512  vitalilem5  25513  vitali  25514  mbfeqalem1  25542  itg1val2  25585  itg10a  25611  itg1ge0a  25612  mbfi1fseqlem4  25619  itg2uba  25644  itg2splitlem  25649  itg2monolem1  25651  itg2cnlem1  25662  itg2cnlem2  25663  itgss  25713  dvtaylp  26278  pserdvlem2  26338  ellogdm  26548  relogbcxp  26695  cxplogb  26696  logbmpt  26698  atandm  26786  atans2  26841  eldmgm  26932  igamgam  26959  igamf  26961  igamcl  26962  lgam1  26974  gam1  26975  wilthlem2  26979  basellem3  26993  fsumvma  27124  dchrelbas2  27148  dchreq  27169  dchrsum  27180  gausslemma2dlem4  27280  2sqreultblem  27359  dchrisum0fno1  27422  rplogsum  27438  newbday  27813  sltlpss  27819  islnopp  28666  frgrncvvdeq  30238  fusgr2wsp2nb  30263  eleigvec  31886  strlem1  32179  strlem5  32184  hstrlem5  32192  difrab2  32427  nfpconfp  32556  fdifsupp  32608  suppiniseg  32609  suppss3  32647  fsuppcurry1  32648  fsuppcurry2  32649  xrdifh  32703  nndiffz1  32709  elrgspnsubrunlem2  33199  ist0cld  33823  ordtconnlem1  33914  esumpinfval  34063  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemb  34359  eulerpartlemf  34361  eulerpartlemt  34362  eulerpartlemgh  34369  ballotlemodife  34489  ballotth  34529  reprdifc  34618  hgt750lemb  34647  onvf1od  35094  elmrsubrn  35507  mrsubvrs  35509  dftr6  35738  dffr5  35741  brsset  35877  dfon3  35880  ellimits  35898  dffun10  35902  elfuns  35903  fullfunfv  35935  dfrecs2  35938  dfrdg4  35939  dfint3  35940  hfext  36171  onsucsuccmpi  36431  bj-rest10b  37077  difunieq  37362  pibt2  37405  iundif1  37588  lindsadd  37607  poimirlem2  37616  poimirlem11  37625  poimirlem12  37626  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem30  37644  itg2addnclem  37665  ftc1anclem5  37691  areacirc  37707  fdc  37739  isfldidl  38062  opelvvdif  38248  iswatN  39988  dochsnkrlem1  41463  unitscyglem4  42186  redvmptabs  42348  selvcllem5  42570  selvvvval  42573  fsuppssindlem1  42579  ellz1  42755  pellexlem4  42820  pellexlem5  42821  ordeldif  43247  ordeldifsucon  43248  ordeldif1o  43249  cantnfresb  43313  cantnf2  43314  oadif1lem  43368  oadif1  43369  infordmin  43521  minregex  43523  pwinfig  43550  elnonrel  43574  sqrtcvallem1  43620  clsk3nimkb  44029  ntrclselnel1  44046  ntrneiel2  44075  ntrneik4w  44089  undif3VD  44871  iindif2f  45154  limcrecl  45627  icccncfext  45885  dvmptfprodlem  45942  stoweidlem26  46024  stoweidlem39  46037  stoweidlem52  46050  fourierdlem42  46147  etransclem18  46250  etransclem46  46278  ovolval4lem1  46647  requad01  47622  dfnbgr6  47857  lindslinindsimp1  48446  dignn0fr  48590