Theorem eldif 3923

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 3484	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3484	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 485	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2857	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2857	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 643	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3916	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3648	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3463   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916

This theorem is referenced by:  eldifd  3924  eldifad  3925  eldifbd  3926  elneeldif  3927  velcomp  3928  difeqri  4091  nfdif  4092  eldifi  4093  eldifn  4094  neldif  4096  difdif  4097  ssconb  4104  sscon  4105  ssdif  4106  raldifb  4111  elsymdif  4219  dfss4  4230  dfun2  4231  dfin2  4232  difin  4233  indifdi  4255  undif3  4261  difin2  4262  ssdif0  4329  difin0ss  4336  inssdif0  4337  reldisj  4419  disj3  4420  undif4  4433  pssnel  4437  inundif  4445  ssundif  4453  eldifpr  4629  elpwunsn  4655  eldiftp  4658  eldifsn  4758  difprsnss  4771  iundif2  5042  iindif1  5045  iindif2  5047  disjss3  5112  brdif  5168  dffr6  5618  difopab  5818  intirr  6119  cnvdif  6141  difxp  6162  xpdifid  6166  xpdifcnvepel  6167  frpoind  6344  ordunidif  6412  onmindif  6456  imadif  6621  dffv2  6977  eldifpw  7767  releldmdifi  8042  funeldmdif  8045  xpord2pred  8141  xpord2indlem  8143  ressuppssdif  8181  extmptsuppeq  8184  suppss  8190  suppssr  8191  suppssrg  8192  suppss2  8196  suppofssd  8199  suppcoss  8203  ondif2  8487  oelim2  8581  eldifsucnn  8650  boxcutc  8939  brsdom  8971  brsdom2  9089  php3  9193  unblem1  9252  unfilem1  9265  elfi2  9374  dfsup2  9404  ordtypelem7  9486  ssttrcl  9684  ttrcltr  9685  dmttrcl  9690  frind  9722  kmlem4  10137  ackbij1lem18  10219  infpssr  10292  isf34lem4  10361  fin17  10378  fin67  10379  dffin7-2  10382  fin1a2lem6  10389  axcclem  10441  pwfseqlem3  10645  grothprim  10819  xrlenlt  11274  nzadd  12642  irradd  12997  irrmul  12998  difreicc  13511  fzdif1  13633  modirr  13978  hashinf  14371  sumss  15775  fsumss  15776  prodss  16001  fprodss  16002  fprodn0f  16045  rpnnen2lem12  16281  dvdsaddre2b  16365  sumeven  16445  bitscmp  16496  lcmfunsnlem2  16698  iserodd  16895  prmodvdslcmf  17107  chnccat  18682  symgfix2  19486  pmtrdifellem4  19549  sylow2alem2  19688  efgsfo  19809  gsumval3  19977  gsum2dlem1  20040  gsum2dlem2  20041  ablfac1eu  20145  gsumdixp  20400  isnirred  20502  isirred2  20503  irredn0  20505  0ringdif  20611  0ring1eq0  20618  lsppratlem1  21249  lbsextlem2  21261  xrsmgmdifsgrp  21528  psgnodpm  21707  mplsubrglem  22122  mplcoe1  22157  mplcoe5  22160  opsrtoslem2  22176  selvcllem5  22259  selvvvval  22262  symgmatr01lem  22779  elcls  23199  isclo  23213  maxlp  23273  restntr  23308  isreg2  23503  cmpcld  23528  hausdiag  23771  txkgen  23778  kqcldsat  23859  ufinffr  24055  fin1aufil  24058  alexsublem  24170  alexsubALTlem3  24175  ptcmplem5  24182  blcld  24631  shftmbl  25666  vitalilem4  25739  vitalilem5  25740  vitali  25741  mbfeqalem1  25769  itg1val2  25812  itg10a  25838  itg1ge0a  25839  mbfi1fseqlem4  25846  itg2uba  25871  itg2splitlem  25876  itg2monolem1  25878  itg2cnlem1  25889  itg2cnlem2  25890  itgss  25940  dvtaylp  26499  pserdvlem2  26557  ellogdm  26770  relogbcxp  26916  cxplogb  26917  logbmpt  26919  atandm  27007  atans2  27062  eldmgm  27152  igamgam  27179  igamf  27181  igamcl  27182  lgam1  27194  gam1  27195  wilthlem2  27199  basellem3  27213  fsumvma  27343  dchrelbas2  27367  dchreq  27388  dchrsum  27399  gausslemma2dlem4  27499  2sqreultblem  27578  dchrisum0fno1  27641  rplogsum  27657  newbday  28061  ltslpss  28067  islnopp  28979  frgrncvvdeq  30601  fusgr2wsp2nb  30626  eleigvec  32250  strlem1  32543  strlem5  32548  hstrlem5  32556  difrab2  32785  nfpconfp  32918  fdifsupp  32971  suppiniseg  32972  suppss3  33009  fsuppcurry1  33010  fsuppcurry2  33011  xrdifh  33066  nndiffz1  33072  elrgspnsubrunlem2  33509  ist0cld  34168  ordtconnlem1  34259  esumpinfval  34408  eulerpartlems  34695  eulerpartlemgc  34697  eulerpartlemb  34703  eulerpartlemf  34705  eulerpartlemt  34706  eulerpartlemgh  34713  ballotlemodife  34833  ballotth  34873  reprdifc  34959  hgt750lemb  34988  onvf1od  35490  elmrsubrn  35911  mrsubvrs  35913  dftr6  36142  dffr5  36145  brsset  36278  dfon3  36281  ellimits  36299  dffun10  36303  elfuns  36304  fullfunfv  36338  dfrecs2  36341  dfrdg4  36342  dfint3  36343  hfext  36574  onsucsuccmpi  36843  bj-rest10b  37619  difunieq  37908  pibt2  37951  iundif1  38133  lindsadd  38152  poimirlem2  38161  poimirlem11  38170  poimirlem12  38171  poimirlem18  38177  poimirlem21  38180  poimirlem22  38181  poimirlem30  38189  itg2addnclem  38210  ftc1anclem5  38236  areacirc  38252  fdc  38284  isfldidl  38607  opelvvdif  38803  iswatN  40658  dochsnkrlem1  42133  unitscyglem4  42855  redvmptabs  43011  fsuppssindlem1  43215  ellz1  43390  pellexlem4  43451  pellexlem5  43452  ordeldif  43877  ordeldifsucon  43878  ordeldif1o  43879  cantnfresb  43943  cantnf2  43944  oadif1lem  43998  oadif1  43999  infordmin  44150  minregex  44152  pwinfig  44179  elnonrel  44203  sqrtcvallem1  44249  clsk3nimkb  44658  ntrclselnel1  44675  ntrneiel2  44704  ntrneik4w  44718  undif3VD  45482  iindif2f  45770  limcrecl  46237  icccncfext  46493  dvmptfprodlem  46550  stoweidlem26  46632  stoweidlem39  46645  stoweidlem52  46658  fourierdlem42  46755  etransclem18  46858  etransclem46  46886  ovolval4lem1  47255  nthrucw  47494  requad01  48275  dfnbgr6  48511  lindslinindsimp1  49122  dignn0fr  49266