Theorem eldif 3927

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920

This theorem is referenced by:  eldifd  3928  eldifad  3929  eldifbd  3930  elneeldif  3931  velcomp  3932  difeqri  4094  nfdif  4095  eldifi  4097  eldifn  4098  neldif  4100  difdif  4101  ddif  4107  ssconb  4108  sscon  4109  ssdif  4110  raldifb  4115  elsymdif  4224  dfss4  4235  dfun2  4236  dfin2  4237  difin  4238  indifdi  4260  undif3  4266  difin2  4267  ssdif0  4332  difin0ss  4339  inssdif0  4340  reldisj  4419  disj3  4420  undif4  4433  pssnel  4437  inundif  4445  ssundif  4454  eldifpr  4625  elpwunsn  4651  eldiftp  4654  eldifsn  4753  difprsnss  4766  iundif2  5041  iindif1  5042  iindif2  5044  disjss3  5109  brdif  5163  dffr6  5597  difopab  5796  difopabOLD  5797  intirr  6094  cnvdif  6119  difxp  6140  xpdifid  6144  frpoind  6318  ordunidif  6385  onmindif  6429  imadif  6603  dffv2  6959  eldifpw  7747  releldmdifi  8027  funeldmdif  8030  xpord2pred  8127  xpord2indlem  8129  ressuppssdif  8167  extmptsuppeq  8170  suppss  8176  suppssr  8177  suppssrg  8178  suppss2  8182  suppofssd  8185  suppcoss  8189  ondif2  8469  oelim2  8562  eldifsucnn  8631  boxcutc  8917  brsdom  8949  brsdom2  9071  php3  9179  unblem1  9246  unfilem1  9261  elfi2  9372  dfsup2  9402  ordtypelem7  9484  ssttrcl  9675  ttrcltr  9676  dmttrcl  9681  frind  9710  kmlem4  10114  ackbij1lem18  10196  infpssr  10268  isf34lem4  10337  fin17  10354  fin67  10355  dffin7-2  10358  fin1a2lem6  10365  axcclem  10417  pwfseqlem3  10620  grothprim  10794  xrlenlt  11246  nzadd  12588  irradd  12939  irrmul  12940  difreicc  13452  fzdif1  13573  modirr  13914  hashinf  14307  sumss  15697  fsumss  15698  prodss  15920  fprodss  15921  fprodn0f  15964  rpnnen2lem12  16200  dvdsaddre2b  16284  sumeven  16364  bitscmp  16415  lcmfunsnlem2  16617  iserodd  16813  prmodvdslcmf  17025  symgfix2  19353  pmtrdifellem4  19416  sylow2alem2  19555  efgsfo  19676  gsumval3  19844  gsum2dlem1  19907  gsum2dlem2  19908  ablfac1eu  20012  gsumdixp  20235  isnirred  20336  isirred2  20337  irredn0  20339  0ringdif  20443  0ring1eq0  20449  lsppratlem1  21064  lbsextlem2  21076  xrsmgmdifsgrp  21327  psgnodpm  21504  mplsubrglem  21920  mplcoe1  21951  mplcoe5  21954  opsrtoslem2  21970  symgmatr01lem  22547  elcls  22967  isclo  22981  maxlp  23041  restntr  23076  isreg2  23271  cmpcld  23296  hausdiag  23539  txkgen  23546  kqcldsat  23627  ufinffr  23823  fin1aufil  23826  alexsublem  23938  alexsubALTlem3  23943  ptcmplem5  23950  blcld  24400  shftmbl  25446  vitalilem4  25519  vitalilem5  25520  vitali  25521  mbfeqalem1  25549  itg1val2  25592  itg10a  25618  itg1ge0a  25619  mbfi1fseqlem4  25626  itg2uba  25651  itg2splitlem  25656  itg2monolem1  25658  itg2cnlem1  25669  itg2cnlem2  25670  itgss  25720  dvtaylp  26285  pserdvlem2  26345  ellogdm  26555  relogbcxp  26702  cxplogb  26703  logbmpt  26705  atandm  26793  atans2  26848  eldmgm  26939  igamgam  26966  igamf  26968  igamcl  26969  lgam1  26981  gam1  26982  wilthlem2  26986  basellem3  27000  fsumvma  27131  dchrelbas2  27155  dchreq  27176  dchrsum  27187  gausslemma2dlem4  27287  2sqreultblem  27366  dchrisum0fno1  27429  rplogsum  27445  newbday  27820  sltlpss  27826  islnopp  28673  frgrncvvdeq  30245  fusgr2wsp2nb  30270  eleigvec  31893  strlem1  32186  strlem5  32191  hstrlem5  32199  difrab2  32434  nfpconfp  32563  fdifsupp  32615  suppiniseg  32616  suppss3  32654  fsuppcurry1  32655  fsuppcurry2  32656  xrdifh  32710  nndiffz1  32716  elrgspnsubrunlem2  33206  ist0cld  33830  ordtconnlem1  33921  esumpinfval  34070  eulerpartlems  34358  eulerpartlemgc  34360  eulerpartlemb  34366  eulerpartlemf  34368  eulerpartlemt  34369  eulerpartlemgh  34376  ballotlemodife  34496  ballotth  34536  reprdifc  34625  hgt750lemb  34654  onvf1od  35101  elmrsubrn  35514  mrsubvrs  35516  dftr6  35745  dffr5  35748  brsset  35884  dfon3  35887  ellimits  35905  dffun10  35909  elfuns  35910  fullfunfv  35942  dfrecs2  35945  dfrdg4  35946  dfint3  35947  hfext  36178  onsucsuccmpi  36438  bj-rest10b  37084  difunieq  37369  pibt2  37412  iundif1  37595  lindsadd  37614  poimirlem2  37623  poimirlem11  37632  poimirlem12  37633  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  poimirlem30  37651  itg2addnclem  37672  ftc1anclem5  37698  areacirc  37714  fdc  37746  isfldidl  38069  opelvvdif  38255  iswatN  39995  dochsnkrlem1  41470  unitscyglem4  42193  redvmptabs  42355  selvcllem5  42577  selvvvval  42580  fsuppssindlem1  42586  ellz1  42762  pellexlem4  42827  pellexlem5  42828  ordeldif  43254  ordeldifsucon  43255  ordeldif1o  43256  cantnfresb  43320  cantnf2  43321  oadif1lem  43375  oadif1  43376  infordmin  43528  minregex  43530  pwinfig  43557  elnonrel  43581  sqrtcvallem1  43627  clsk3nimkb  44036  ntrclselnel1  44053  ntrneiel2  44082  ntrneik4w  44096  undif3VD  44878  iindif2f  45161  limcrecl  45634  icccncfext  45892  dvmptfprodlem  45949  stoweidlem26  46031  stoweidlem39  46044  stoweidlem52  46057  fourierdlem42  46154  etransclem18  46257  etransclem46  46285  ovolval4lem1  46654  requad01  47626  dfnbgr6  47861  lindslinindsimp1  48450  dignn0fr  48594