Theorem eldif 3907

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∖ cdif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900

This theorem is referenced by:  eldifd  3908  eldifad  3909  eldifbd  3910  elneeldif  3911  velcomp  3912  difeqri  4075  nfdif  4076  eldifi  4078  eldifn  4079  neldif  4081  difdif  4082  ddif  4088  ssconb  4089  sscon  4090  ssdif  4091  raldifb  4096  elsymdif  4205  dfss4  4216  dfun2  4217  dfin2  4218  difin  4219  indifdi  4241  undif3  4247  difin2  4248  ssdif0  4313  difin0ss  4320  inssdif0  4321  reldisj  4400  disj3  4401  undif4  4414  pssnel  4418  inundif  4426  ssundif  4435  eldifpr  4608  elpwunsn  4634  eldiftp  4637  eldifsn  4735  difprsnss  4748  iundif2  5020  iindif1  5021  iindif2  5023  disjss3  5088  brdif  5142  dffr6  5570  difopab  5769  intirr  6064  cnvdif  6090  difxp  6111  xpdifid  6115  frpoind  6289  ordunidif  6356  onmindif  6400  imadif  6565  dffv2  6917  eldifpw  7701  releldmdifi  7977  funeldmdif  7980  xpord2pred  8075  xpord2indlem  8077  ressuppssdif  8115  extmptsuppeq  8118  suppss  8124  suppssr  8125  suppssrg  8126  suppss2  8130  suppofssd  8133  suppcoss  8137  ondif2  8417  oelim2  8510  eldifsucnn  8579  boxcutc  8865  brsdom  8897  brsdom2  9014  php3  9118  unblem1  9176  unfilem1  9189  elfi2  9298  dfsup2  9328  ordtypelem7  9410  ssttrcl  9605  ttrcltr  9606  dmttrcl  9611  frind  9643  kmlem4  10045  ackbij1lem18  10127  infpssr  10199  isf34lem4  10268  fin17  10285  fin67  10286  dffin7-2  10289  fin1a2lem6  10296  axcclem  10348  pwfseqlem3  10551  grothprim  10725  xrlenlt  11177  nzadd  12520  irradd  12871  irrmul  12872  difreicc  13384  fzdif1  13505  modirr  13849  hashinf  14242  sumss  15631  fsumss  15632  prodss  15854  fprodss  15855  fprodn0f  15898  rpnnen2lem12  16134  dvdsaddre2b  16218  sumeven  16298  bitscmp  16349  lcmfunsnlem2  16551  iserodd  16747  prmodvdslcmf  16959  chnccat  18532  symgfix2  19328  pmtrdifellem4  19391  sylow2alem2  19530  efgsfo  19651  gsumval3  19819  gsum2dlem1  19882  gsum2dlem2  19883  ablfac1eu  19987  gsumdixp  20237  isnirred  20338  isirred2  20339  irredn0  20341  0ringdif  20442  0ring1eq0  20448  lsppratlem1  21084  lbsextlem2  21096  xrsmgmdifsgrp  21345  psgnodpm  21525  mplsubrglem  21941  mplcoe1  21972  mplcoe5  21975  opsrtoslem2  21991  symgmatr01lem  22568  elcls  22988  isclo  23002  maxlp  23062  restntr  23097  isreg2  23292  cmpcld  23317  hausdiag  23560  txkgen  23567  kqcldsat  23648  ufinffr  23844  fin1aufil  23847  alexsublem  23959  alexsubALTlem3  23964  ptcmplem5  23971  blcld  24420  shftmbl  25466  vitalilem4  25539  vitalilem5  25540  vitali  25541  mbfeqalem1  25569  itg1val2  25612  itg10a  25638  itg1ge0a  25639  mbfi1fseqlem4  25646  itg2uba  25671  itg2splitlem  25676  itg2monolem1  25678  itg2cnlem1  25689  itg2cnlem2  25690  itgss  25740  dvtaylp  26305  pserdvlem2  26365  ellogdm  26575  relogbcxp  26722  cxplogb  26723  logbmpt  26725  atandm  26813  atans2  26868  eldmgm  26959  igamgam  26986  igamf  26988  igamcl  26989  lgam1  27001  gam1  27002  wilthlem2  27006  basellem3  27020  fsumvma  27151  dchrelbas2  27175  dchreq  27196  dchrsum  27207  gausslemma2dlem4  27307  2sqreultblem  27386  dchrisum0fno1  27449  rplogsum  27465  newbday  27847  sltlpss  27853  islnopp  28717  frgrncvvdeq  30289  fusgr2wsp2nb  30314  eleigvec  31937  strlem1  32230  strlem5  32235  hstrlem5  32243  difrab2  32477  nfpconfp  32614  fdifsupp  32666  suppiniseg  32667  suppss3  32706  fsuppcurry1  32707  fsuppcurry2  32708  xrdifh  32763  nndiffz1  32769  elrgspnsubrunlem2  33215  ist0cld  33846  ordtconnlem1  33937  esumpinfval  34086  eulerpartlems  34373  eulerpartlemgc  34375  eulerpartlemb  34381  eulerpartlemf  34383  eulerpartlemt  34384  eulerpartlemgh  34391  ballotlemodife  34511  ballotth  34551  reprdifc  34640  hgt750lemb  34669  onvf1od  35151  elmrsubrn  35564  mrsubvrs  35566  dftr6  35795  dffr5  35798  brsset  35931  dfon3  35934  ellimits  35952  dffun10  35956  elfuns  35957  fullfunfv  35991  dfrecs2  35994  dfrdg4  35995  dfint3  35996  hfext  36227  onsucsuccmpi  36487  bj-rest10b  37133  difunieq  37418  pibt2  37461  iundif1  37644  lindsadd  37663  poimirlem2  37672  poimirlem11  37681  poimirlem12  37682  poimirlem18  37688  poimirlem21  37691  poimirlem22  37692  poimirlem30  37700  itg2addnclem  37721  ftc1anclem5  37747  areacirc  37763  fdc  37795  isfldidl  38118  opelvvdif  38306  iswatN  40103  dochsnkrlem1  41578  unitscyglem4  42301  redvmptabs  42463  selvcllem5  42685  selvvvval  42688  fsuppssindlem1  42694  ellz1  42870  pellexlem4  42935  pellexlem5  42936  ordeldif  43361  ordeldifsucon  43362  ordeldif1o  43363  cantnfresb  43427  cantnf2  43428  oadif1lem  43482  oadif1  43483  infordmin  43635  minregex  43637  pwinfig  43664  elnonrel  43688  sqrtcvallem1  43734  clsk3nimkb  44143  ntrclselnel1  44160  ntrneiel2  44189  ntrneik4w  44203  undif3VD  44984  iindif2f  45267  limcrecl  45739  icccncfext  45995  dvmptfprodlem  46052  stoweidlem26  46134  stoweidlem39  46147  stoweidlem52  46160  fourierdlem42  46257  etransclem18  46360  etransclem46  46388  ovolval4lem1  46757  nthrucw  46994  requad01  47731  dfnbgr6  47967  lindslinindsimp1  48568  dignn0fr  48712