Theorem eldif 3893

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 3452	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3452	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2827	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2827	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 319	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 638	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3886	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3618	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 379	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886

This theorem is referenced by:  eldifd  3894  eldifad  3895  eldifbd  3896  elneeldif  3897  velcomp  3898  difeqri  4059  nfdif  4060  eldifi  4061  eldifn  4062  neldif  4064  difdif  4065  ssconb  4072  sscon  4073  ssdif  4074  raldifb  4079  elsymdif  4186  dfss4  4197  dfun2  4198  dfin2  4199  difin  4200  indifdi  4222  undif3  4228  difin2  4229  ssdif0  4294  difin0ss  4301  inssdif0  4302  reldisj  4381  disj3  4382  undif4  4395  pssnel  4399  inundif  4407  ssundif  4415  eldifpr  4590  elpwunsn  4616  eldiftp  4619  eldifsn  4719  difprsnss  4732  iundif2  5003  iindif1  5004  iindif2  5006  disjss3  5071  brdif  5125  dffr6  5574  difopab  5773  intirr  6068  cnvdif  6094  difxp  6115  xpdifid  6119  frpoind  6293  ordunidif  6360  onmindif  6404  imadif  6569  dffv2  6922  eldifpw  7711  releldmdifi  7987  funeldmdif  7990  xpord2pred  8085  xpord2indlem  8087  ressuppssdif  8125  extmptsuppeq  8128  suppss  8134  suppssr  8135  suppssrg  8136  suppss2  8140  suppofssd  8143  suppcoss  8147  ondif2  8427  oelim2  8521  eldifsucnn  8590  boxcutc  8879  brsdom  8911  brsdom2  9029  php3  9133  unblem1  9192  unfilem1  9205  elfi2  9317  dfsup2  9347  ordtypelem7  9429  ssttrcl  9627  ttrcltr  9628  dmttrcl  9633  frind  9665  kmlem4  10067  ackbij1lem18  10149  infpssr  10221  isf34lem4  10290  fin17  10307  fin67  10308  dffin7-2  10311  fin1a2lem6  10318  axcclem  10370  pwfseqlem3  10574  grothprim  10748  xrlenlt  11201  nzadd  12566  irradd  12914  irrmul  12915  difreicc  13428  fzdif1  13550  modirr  13895  hashinf  14288  sumss  15677  fsumss  15678  prodss  15903  fprodss  15904  fprodn0f  15947  rpnnen2lem12  16183  dvdsaddre2b  16267  sumeven  16347  bitscmp  16398  lcmfunsnlem2  16600  iserodd  16797  prmodvdslcmf  17009  chnccat  18583  symgfix2  19382  pmtrdifellem4  19445  sylow2alem2  19584  efgsfo  19705  gsumval3  19873  gsum2dlem1  19936  gsum2dlem2  19937  ablfac1eu  20041  gsumdixp  20289  isnirred  20391  isirred2  20392  irredn0  20394  0ringdif  20499  0ring1eq0  20505  lsppratlem1  21140  lbsextlem2  21152  xrsmgmdifsgrp  21384  psgnodpm  21563  mplsubrglem  21978  mplcoe1  22013  mplcoe5  22016  opsrtoslem2  22032  selvcllem5  22115  selvvvval  22118  symgmatr01lem  22636  elcls  23056  isclo  23070  maxlp  23130  restntr  23165  isreg2  23360  cmpcld  23385  hausdiag  23628  txkgen  23635  kqcldsat  23716  ufinffr  23912  fin1aufil  23915  alexsublem  24027  alexsubALTlem3  24032  ptcmplem5  24039  blcld  24488  shftmbl  25523  vitalilem4  25596  vitalilem5  25597  vitali  25598  mbfeqalem1  25626  itg1val2  25669  itg10a  25695  itg1ge0a  25696  mbfi1fseqlem4  25703  itg2uba  25728  itg2splitlem  25733  itg2monolem1  25735  itg2cnlem1  25746  itg2cnlem2  25747  itgss  25797  dvtaylp  26353  pserdvlem2  26411  ellogdm  26621  relogbcxp  26767  cxplogb  26768  logbmpt  26770  atandm  26858  atans2  26913  eldmgm  27003  igamgam  27030  igamf  27032  igamcl  27033  lgam1  27045  gam1  27046  wilthlem2  27050  basellem3  27064  fsumvma  27194  dchrelbas2  27218  dchreq  27239  dchrsum  27250  gausslemma2dlem4  27350  2sqreultblem  27429  dchrisum0fno1  27492  rplogsum  27508  newbday  27912  ltslpss  27918  islnopp  28825  frgrncvvdeq  30397  fusgr2wsp2nb  30422  eleigvec  32046  strlem1  32339  strlem5  32344  hstrlem5  32352  difrab2  32585  nfpconfp  32724  fdifsupp  32777  suppiniseg  32778  suppss3  32815  fsuppcurry1  32816  fsuppcurry2  32817  xrdifh  32872  nndiffz1  32878  elrgspnsubrunlem2  33329  ist0cld  34017  ordtconnlem1  34108  esumpinfval  34257  eulerpartlems  34544  eulerpartlemgc  34546  eulerpartlemb  34552  eulerpartlemf  34554  eulerpartlemt  34555  eulerpartlemgh  34562  ballotlemodife  34682  ballotth  34722  reprdifc  34811  hgt750lemb  34840  onvf1od  35335  elmrsubrn  35748  mrsubvrs  35750  dftr6  35979  dffr5  35982  brsset  36115  dfon3  36118  ellimits  36136  dffun10  36140  elfuns  36141  fullfunfv  36175  dfrecs2  36178  dfrdg4  36179  dfint3  36180  hfext  36411  onsucsuccmpi  36671  bj-rest10b  37447  difunieq  37736  pibt2  37779  iundif1  37961  lindsadd  37980  poimirlem2  37989  poimirlem11  37998  poimirlem12  37999  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  poimirlem30  38017  itg2addnclem  38038  ftc1anclem5  38064  areacirc  38080  fdc  38112  isfldidl  38435  opelvvdif  38631  iswatN  40486  dochsnkrlem1  41961  unitscyglem4  42683  redvmptabs  42837  fsuppssindlem1  43041  ellz1  43216  pellexlem4  43277  pellexlem5  43278  ordeldif  43703  ordeldifsucon  43704  ordeldif1o  43705  cantnfresb  43769  cantnf2  43770  oadif1lem  43824  oadif1  43825  infordmin  43976  minregex  43978  pwinfig  44005  elnonrel  44029  sqrtcvallem1  44075  clsk3nimkb  44484  ntrclselnel1  44501  ntrneiel2  44530  ntrneik4w  44544  undif3VD  45325  iindif2f  45607  limcrecl  46074  icccncfext  46330  dvmptfprodlem  46387  stoweidlem26  46469  stoweidlem39  46482  stoweidlem52  46495  fourierdlem42  46592  etransclem18  46695  etransclem46  46723  ovolval4lem1  47092  nthrucw  47331  requad01  48112  dfnbgr6  48348  lindslinindsimp1  48948  dignn0fr  49092