Theorem eldif 3914

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 3475	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3475	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 484	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2850	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2850	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 320	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 641	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3907	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3639	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 380	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  Vcvv 3454   ∖ cdif 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907

This theorem is referenced by:  eldifd  3915  eldifad  3916  eldifbd  3917  elneeldif  3918  velcomp  3919  difeqri  4082  nfdif  4083  eldifi  4084  eldifn  4085  neldif  4087  difdif  4088  ssconb  4095  sscon  4096  ssdif  4097  raldifb  4102  elsymdif  4210  dfss4  4221  dfun2  4222  dfin2  4223  difin  4224  indifdi  4246  undif3  4252  difin2  4253  ssdif0  4319  difin0ss  4326  inssdif0  4327  reldisj  4407  disj3  4408  undif4  4421  pssnel  4425  inundif  4433  ssundif  4441  eldifpr  4617  elpwunsn  4643  eldiftp  4646  eldifsn  4746  difprsnss  4759  iundif2  5031  iindif1  5032  iindif2  5034  disjss3  5099  brdif  5153  dffr6  5603  difopab  5803  intirr  6105  cnvdif  6127  difxp  6149  xpdifid  6153  xpdifcnvepel  6154  frpoind  6329  ordunidif  6396  onmindif  6440  imadif  6605  dffv2  6962  eldifpw  7751  releldmdifi  8026  funeldmdif  8029  xpord2pred  8125  xpord2indlem  8127  ressuppssdif  8165  extmptsuppeq  8168  suppss  8174  suppssr  8175  suppssrg  8176  suppss2  8180  suppofssd  8183  suppcoss  8187  ondif2  8471  oelim2  8565  eldifsucnn  8634  boxcutc  8923  brsdom  8955  brsdom2  9073  php3  9177  unblem1  9236  unfilem1  9249  elfi2  9360  dfsup2  9390  ordtypelem7  9472  ssttrcl  9670  ttrcltr  9671  dmttrcl  9676  frind  9708  kmlem4  10110  ackbij1lem18  10192  infpssr  10265  isf34lem4  10334  fin17  10351  fin67  10352  dffin7-2  10355  fin1a2lem6  10362  axcclem  10414  pwfseqlem3  10618  grothprim  10792  xrlenlt  11247  nzadd  12619  irradd  12974  irrmul  12975  difreicc  13488  fzdif1  13610  modirr  13955  hashinf  14348  sumss  15751  fsumss  15752  prodss  15977  fprodss  15978  fprodn0f  16021  rpnnen2lem12  16257  dvdsaddre2b  16341  sumeven  16421  bitscmp  16472  lcmfunsnlem2  16674  iserodd  16871  prmodvdslcmf  17083  chnccat  18658  symgfix2  19456  pmtrdifellem4  19519  sylow2alem2  19658  efgsfo  19779  gsumval3  19947  gsum2dlem1  20010  gsum2dlem2  20011  ablfac1eu  20115  gsumdixp  20367  isnirred  20469  isirred2  20470  irredn0  20472  0ringdif  20577  0ring1eq0  20583  lsppratlem1  21217  lbsextlem2  21229  xrsmgmdifsgrp  21461  psgnodpm  21640  mplsubrglem  22055  mplcoe1  22090  mplcoe5  22093  opsrtoslem2  22109  selvcllem5  22192  selvvvval  22195  symgmatr01lem  22713  elcls  23133  isclo  23147  maxlp  23207  restntr  23242  isreg2  23437  cmpcld  23462  hausdiag  23705  txkgen  23712  kqcldsat  23793  ufinffr  23989  fin1aufil  23992  alexsublem  24104  alexsubALTlem3  24109  ptcmplem5  24116  blcld  24565  shftmbl  25600  vitalilem4  25673  vitalilem5  25674  vitali  25675  mbfeqalem1  25703  itg1val2  25746  itg10a  25772  itg1ge0a  25773  mbfi1fseqlem4  25780  itg2uba  25805  itg2splitlem  25810  itg2monolem1  25812  itg2cnlem1  25823  itg2cnlem2  25824  itgss  25874  dvtaylp  26433  pserdvlem2  26491  ellogdm  26704  relogbcxp  26850  cxplogb  26851  logbmpt  26853  atandm  26941  atans2  26996  eldmgm  27086  igamgam  27113  igamf  27115  igamcl  27116  lgam1  27128  gam1  27129  wilthlem2  27133  basellem3  27147  fsumvma  27277  dchrelbas2  27301  dchreq  27322  dchrsum  27333  gausslemma2dlem4  27433  2sqreultblem  27512  dchrisum0fno1  27575  rplogsum  27591  newbday  27995  ltslpss  28001  islnopp  28912  frgrncvvdeq  30511  fusgr2wsp2nb  30536  eleigvec  32160  strlem1  32453  strlem5  32458  hstrlem5  32466  difrab2  32697  nfpconfp  32834  fdifsupp  32887  suppiniseg  32888  suppss3  32925  fsuppcurry1  32926  fsuppcurry2  32927  xrdifh  32982  nndiffz1  32988  elrgspnsubrunlem2  33429  ist0cld  34130  ordtconnlem1  34221  esumpinfval  34370  eulerpartlems  34657  eulerpartlemgc  34659  eulerpartlemb  34665  eulerpartlemf  34667  eulerpartlemt  34668  eulerpartlemgh  34675  ballotlemodife  34795  ballotth  34835  reprdifc  34921  hgt750lemb  34950  onvf1od  35450  elmrsubrn  35870  mrsubvrs  35872  dftr6  36101  dffr5  36104  brsset  36237  dfon3  36240  ellimits  36258  dffun10  36262  elfuns  36263  fullfunfv  36297  dfrecs2  36300  dfrdg4  36301  dfint3  36302  hfext  36533  onsucsuccmpi  36803  bj-rest10b  37579  difunieq  37868  pibt2  37911  iundif1  38093  lindsadd  38112  poimirlem2  38121  poimirlem11  38130  poimirlem12  38131  poimirlem18  38137  poimirlem21  38140  poimirlem22  38141  poimirlem30  38149  itg2addnclem  38170  ftc1anclem5  38196  areacirc  38212  fdc  38244  isfldidl  38567  opelvvdif  38763  iswatN  40618  dochsnkrlem1  42093  unitscyglem4  42815  redvmptabs  42969  fsuppssindlem1  43173  ellz1  43348  pellexlem4  43409  pellexlem5  43410  ordeldif  43835  ordeldifsucon  43836  ordeldif1o  43837  cantnfresb  43901  cantnf2  43902  oadif1lem  43956  oadif1  43957  infordmin  44108  minregex  44110  pwinfig  44137  elnonrel  44161  sqrtcvallem1  44207  clsk3nimkb  44616  ntrclselnel1  44633  ntrneiel2  44662  ntrneik4w  44676  undif3VD  45457  iindif2f  45738  limcrecl  46205  icccncfext  46461  dvmptfprodlem  46518  stoweidlem26  46600  stoweidlem39  46613  stoweidlem52  46626  fourierdlem42  46723  etransclem18  46826  etransclem46  46854  ovolval4lem1  47223  nthrucw  47462  requad01  48243  dfnbgr6  48479  lindslinindsimp1  49079  dignn0fr  49223