Theorem eldif 3961

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ∖ cdif 3948

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954

This theorem is referenced by:  eldifd  3962  eldifad  3963  eldifbd  3964  elneeldif  3965  velcomp  3966  difeqri  4128  nfdif  4129  eldifi  4131  eldifn  4132  neldif  4134  difdif  4135  ddif  4141  ssconb  4142  sscon  4143  ssdif  4144  raldifb  4149  elsymdif  4258  dfss4  4269  dfun2  4270  dfin2  4271  difin  4272  indifdi  4294  undif3  4300  difin2  4301  ssdif0  4366  difin0ss  4373  inssdif0  4374  reldisj  4453  disj3  4454  undif4  4467  pssnel  4471  inundif  4479  ssundif  4488  eldifpr  4658  elpwunsn  4684  eldiftp  4687  eldifsn  4786  difprsnss  4799  iundif2  5074  iindif1  5075  iindif2  5077  disjss3  5142  brdif  5196  dffr6  5640  difopab  5840  difopabOLD  5841  intirr  6138  cnvdif  6163  difxp  6184  xpdifid  6188  frpoind  6363  wfiOLD  6372  ordunidif  6433  onmindif  6476  imadif  6650  dffv2  7004  eldifpw  7788  releldmdifi  8070  funeldmdif  8073  xpord2pred  8170  xpord2indlem  8172  ressuppssdif  8210  extmptsuppeq  8213  suppss  8219  suppssr  8220  suppssrg  8221  suppss2  8225  suppofssd  8228  suppcoss  8232  ondif2  8540  oelim2  8633  eldifsucnn  8702  boxcutc  8981  brsdom  9015  brsdom2  9137  php3  9249  php3OLD  9261  unblem1  9328  unfilem1  9343  elfi2  9454  dfsup2  9484  ordtypelem7  9564  ssttrcl  9755  ttrcltr  9756  dmttrcl  9761  frind  9790  kmlem4  10194  ackbij1lem18  10276  infpssr  10348  isf34lem4  10417  fin17  10434  fin67  10435  dffin7-2  10438  fin1a2lem6  10445  axcclem  10497  pwfseqlem3  10700  grothprim  10874  xrlenlt  11326  nzadd  12665  irradd  13015  irrmul  13016  difreicc  13524  fzdif1  13645  modirr  13983  hashinf  14374  sumss  15760  fsumss  15761  prodss  15983  fprodss  15984  fprodn0f  16027  rpnnen2lem12  16261  dvdsaddre2b  16344  sumeven  16424  bitscmp  16475  lcmfunsnlem2  16677  iserodd  16873  prmodvdslcmf  17085  symgfix2  19434  pmtrdifellem4  19497  sylow2alem2  19636  efgsfo  19757  gsumval3  19925  gsum2dlem1  19988  gsum2dlem2  19989  ablfac1eu  20093  gsumdixp  20316  isnirred  20420  isirred2  20421  irredn0  20423  0ringdif  20527  0ring1eq0  20533  lsppratlem1  21149  lbsextlem2  21161  xrsmgmdifsgrp  21421  psgnodpm  21606  mplsubrglem  22024  mplcoe1  22055  mplcoe5  22058  opsrtoslem2  22080  symgmatr01lem  22659  elcls  23081  isclo  23095  maxlp  23155  restntr  23190  isreg2  23385  cmpcld  23410  hausdiag  23653  txkgen  23660  kqcldsat  23741  ufinffr  23937  fin1aufil  23940  alexsublem  24052  alexsubALTlem3  24057  ptcmplem5  24064  blcld  24518  shftmbl  25573  vitalilem4  25646  vitalilem5  25647  vitali  25648  mbfeqalem1  25676  itg1val2  25719  itg10a  25745  itg1ge0a  25746  mbfi1fseqlem4  25753  itg2uba  25778  itg2splitlem  25783  itg2monolem1  25785  itg2cnlem1  25796  itg2cnlem2  25797  itgss  25847  dvtaylp  26412  pserdvlem2  26472  ellogdm  26681  relogbcxp  26828  cxplogb  26829  logbmpt  26831  atandm  26919  atans2  26974  eldmgm  27065  igamgam  27092  igamf  27094  igamcl  27095  lgam1  27107  gam1  27108  wilthlem2  27112  basellem3  27126  fsumvma  27257  dchrelbas2  27281  dchreq  27302  dchrsum  27313  gausslemma2dlem4  27413  2sqreultblem  27492  dchrisum0fno1  27555  rplogsum  27571  newbday  27940  sltlpss  27945  islnopp  28747  frgrncvvdeq  30328  fusgr2wsp2nb  30353  eleigvec  31976  strlem1  32269  strlem5  32274  hstrlem5  32282  difrab2  32517  nfpconfp  32642  fdifsupp  32694  suppiniseg  32695  suppss3  32735  fsuppcurry1  32736  fsuppcurry2  32737  xrdifh  32782  nndiffz1  32788  elrgspnsubrunlem2  33252  ist0cld  33832  ordtconnlem1  33923  esumpinfval  34074  eulerpartlems  34362  eulerpartlemgc  34364  eulerpartlemb  34370  eulerpartlemf  34372  eulerpartlemt  34373  eulerpartlemgh  34380  ballotlemodife  34500  ballotth  34540  reprdifc  34642  hgt750lemb  34671  elmrsubrn  35525  mrsubvrs  35527  dftr6  35751  dffr5  35754  brsset  35890  dfon3  35893  ellimits  35911  dffun10  35915  elfuns  35916  fullfunfv  35948  dfrecs2  35951  dfrdg4  35952  dfint3  35953  hfext  36184  onsucsuccmpi  36444  bj-rest10b  37090  difunieq  37375  pibt2  37418  iundif1  37601  lindsadd  37620  poimirlem2  37629  poimirlem11  37638  poimirlem12  37639  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem30  37657  itg2addnclem  37678  ftc1anclem5  37704  areacirc  37720  fdc  37752  isfldidl  38075  opelvvdif  38260  iswatN  39996  dochsnkrlem1  41471  unitscyglem4  42199  redvmptabs  42390  selvcllem5  42592  selvvvval  42595  fsuppssindlem1  42601  ellz1  42778  pellexlem4  42843  pellexlem5  42844  ordeldif  43271  ordeldifsucon  43272  ordeldif1o  43273  cantnfresb  43337  cantnf2  43338  oadif1lem  43392  oadif1  43393  infordmin  43545  minregex  43547  pwinfig  43574  elnonrel  43598  sqrtcvallem1  43644  clsk3nimkb  44053  ntrclselnel1  44070  ntrneiel2  44099  ntrneik4w  44113  undif3VD  44902  iindif2f  45165  limcrecl  45644  icccncfext  45902  dvmptfprodlem  45959  stoweidlem26  46041  stoweidlem39  46054  stoweidlem52  46067  fourierdlem42  46164  etransclem18  46267  etransclem46  46295  ovolval4lem1  46664  requad01  47608  dfnbgr6  47843  lindslinindsimp1  48374  dignn0fr  48522