Theorem eldif 3921

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 3465	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3465	. . 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 3914	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3644	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

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

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 3446  df-dif 3914

This theorem is referenced by:  eldifd  3922  eldifad  3923  eldifbd  3924  elneeldif  3925  velcomp  3926  difeqri  4087  nfdif  4088  eldifi  4090  eldifn  4091  neldif  4093  difdif  4094  ddif  4100  ssconb  4101  sscon  4102  ssdif  4103  raldifb  4108  elsymdif  4217  dfss4  4228  dfun2  4229  dfin2  4230  difin  4231  indifdi  4253  undif3  4259  difin2  4260  ssdif0  4325  difin0ss  4332  inssdif0  4333  reldisj  4412  disj3  4413  undif4  4426  pssnel  4430  inundif  4438  ssundif  4447  eldifpr  4618  elpwunsn  4644  eldiftp  4647  eldifsn  4746  difprsnss  4759  iundif2  5033  iindif1  5034  iindif2  5036  disjss3  5101  brdif  5155  dffr6  5587  difopab  5784  intirr  6079  cnvdif  6104  difxp  6125  xpdifid  6129  frpoind  6303  ordunidif  6370  onmindif  6414  imadif  6584  dffv2  6938  eldifpw  7724  releldmdifi  8003  funeldmdif  8006  xpord2pred  8101  xpord2indlem  8103  ressuppssdif  8141  extmptsuppeq  8144  suppss  8150  suppssr  8151  suppssrg  8152  suppss2  8156  suppofssd  8159  suppcoss  8163  ondif2  8443  oelim2  8536  eldifsucnn  8605  boxcutc  8891  brsdom  8923  brsdom2  9042  php3  9150  unblem1  9215  unfilem1  9230  elfi2  9341  dfsup2  9371  ordtypelem7  9453  ssttrcl  9644  ttrcltr  9645  dmttrcl  9650  frind  9679  kmlem4  10083  ackbij1lem18  10165  infpssr  10237  isf34lem4  10306  fin17  10323  fin67  10324  dffin7-2  10327  fin1a2lem6  10334  axcclem  10386  pwfseqlem3  10589  grothprim  10763  xrlenlt  11215  nzadd  12557  irradd  12908  irrmul  12909  difreicc  13421  fzdif1  13542  modirr  13883  hashinf  14276  sumss  15666  fsumss  15667  prodss  15889  fprodss  15890  fprodn0f  15933  rpnnen2lem12  16169  dvdsaddre2b  16253  sumeven  16333  bitscmp  16384  lcmfunsnlem2  16586  iserodd  16782  prmodvdslcmf  16994  symgfix2  19330  pmtrdifellem4  19393  sylow2alem2  19532  efgsfo  19653  gsumval3  19821  gsum2dlem1  19884  gsum2dlem2  19885  ablfac1eu  19989  gsumdixp  20239  isnirred  20340  isirred2  20341  irredn0  20343  0ringdif  20447  0ring1eq0  20453  lsppratlem1  21089  lbsextlem2  21101  xrsmgmdifsgrp  21350  psgnodpm  21530  mplsubrglem  21946  mplcoe1  21977  mplcoe5  21980  opsrtoslem2  21996  symgmatr01lem  22573  elcls  22993  isclo  23007  maxlp  23067  restntr  23102  isreg2  23297  cmpcld  23322  hausdiag  23565  txkgen  23572  kqcldsat  23653  ufinffr  23849  fin1aufil  23852  alexsublem  23964  alexsubALTlem3  23969  ptcmplem5  23976  blcld  24426  shftmbl  25472  vitalilem4  25545  vitalilem5  25546  vitali  25547  mbfeqalem1  25575  itg1val2  25618  itg10a  25644  itg1ge0a  25645  mbfi1fseqlem4  25652  itg2uba  25677  itg2splitlem  25682  itg2monolem1  25684  itg2cnlem1  25695  itg2cnlem2  25696  itgss  25746  dvtaylp  26311  pserdvlem2  26371  ellogdm  26581  relogbcxp  26728  cxplogb  26729  logbmpt  26731  atandm  26819  atans2  26874  eldmgm  26965  igamgam  26992  igamf  26994  igamcl  26995  lgam1  27007  gam1  27008  wilthlem2  27012  basellem3  27026  fsumvma  27157  dchrelbas2  27181  dchreq  27202  dchrsum  27213  gausslemma2dlem4  27313  2sqreultblem  27392  dchrisum0fno1  27455  rplogsum  27471  newbday  27851  sltlpss  27857  islnopp  28719  frgrncvvdeq  30288  fusgr2wsp2nb  30313  eleigvec  31936  strlem1  32229  strlem5  32234  hstrlem5  32242  difrab2  32477  nfpconfp  32606  fdifsupp  32658  suppiniseg  32659  suppss3  32697  fsuppcurry1  32698  fsuppcurry2  32699  xrdifh  32753  nndiffz1  32759  elrgspnsubrunlem2  33215  ist0cld  33816  ordtconnlem1  33907  esumpinfval  34056  eulerpartlems  34344  eulerpartlemgc  34346  eulerpartlemb  34352  eulerpartlemf  34354  eulerpartlemt  34355  eulerpartlemgh  34362  ballotlemodife  34482  ballotth  34522  reprdifc  34611  hgt750lemb  34640  onvf1od  35087  elmrsubrn  35500  mrsubvrs  35502  dftr6  35731  dffr5  35734  brsset  35870  dfon3  35873  ellimits  35891  dffun10  35895  elfuns  35896  fullfunfv  35928  dfrecs2  35931  dfrdg4  35932  dfint3  35933  hfext  36164  onsucsuccmpi  36424  bj-rest10b  37070  difunieq  37355  pibt2  37398  iundif1  37581  lindsadd  37600  poimirlem2  37609  poimirlem11  37618  poimirlem12  37619  poimirlem18  37625  poimirlem21  37628  poimirlem22  37629  poimirlem30  37637  itg2addnclem  37658  ftc1anclem5  37684  areacirc  37700  fdc  37732  isfldidl  38055  opelvvdif  38241  iswatN  39981  dochsnkrlem1  41456  unitscyglem4  42179  redvmptabs  42341  selvcllem5  42563  selvvvval  42566  fsuppssindlem1  42572  ellz1  42748  pellexlem4  42813  pellexlem5  42814  ordeldif  43240  ordeldifsucon  43241  ordeldif1o  43242  cantnfresb  43306  cantnf2  43307  oadif1lem  43361  oadif1  43362  infordmin  43514  minregex  43516  pwinfig  43543  elnonrel  43567  sqrtcvallem1  43613  clsk3nimkb  44022  ntrclselnel1  44039  ntrneiel2  44068  ntrneik4w  44082  undif3VD  44864  iindif2f  45147  limcrecl  45620  icccncfext  45878  dvmptfprodlem  45935  stoweidlem26  46017  stoweidlem39  46030  stoweidlem52  46043  fourierdlem42  46140  etransclem18  46243  etransclem46  46271  ovolval4lem1  46640  requad01  47615  dfnbgr6  47850  lindslinindsimp1  48439  dignn0fr  48583