Theorem eldif 3909

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 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2848	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2848	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3902	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3634	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902

This theorem is used by:  eldifd  3910  eldifad  3911  eldifbd  3912  elneeldif  3913  velcomp  3914  difeqri  4076  nfdif  4077  eldifi  4078  eldifn  4079  neldif  4081  difdif  4082  ssconb  4089  sscon  4090  ssdif  4091  raldifb  4096  elsymdif  4204  dfss4  4215  dfun2  4216  dfin2  4217  difin  4218  indifdi  4240  undif3  4246  difin2  4247  ssdif0  4314  difin0ss  4321  inssdif0OLD  4323  reldisj  4406  disj3  4407  undif4  4420  pssnel  4424  inundif  4435  ssundif  4443  eldifpr  4619  elpwunsn  4645  eldiftp  4648  eldifsn  4748  difprsnss  4762  iundif2  5032  iindif1  5035  iindif2  5037  disjss3  5102  brdif  5158  dffr6  5611  difopab  5811  intirr  6112  cnvdif  6134  difxp  6156  xpdifid  6160  xpdifcnvepel  6161  frpoind  6340  ordunidif  6408  onmindif  6452  imadif  6618  dffv2  6974  eldifpw  7768  releldmdifi  8043  funeldmdif  8046  xpord2pred  8144  xpord2indlem  8146  ressuppssdif  8184  extmptsuppeq  8187  suppss  8193  suppssr  8194  suppssrg  8195  suppss2  8199  suppofssd  8202  suppcoss  8206  ondif2  8492  oelim2  8586  eldifsucnn  8655  boxcutc  8951  brsdom  8983  brsdom2  9102  php3  9206  unblem1  9265  unfilem1  9278  elfi2  9387  dfsup2  9417  ordtypelem7  9499  ssttrcl  9697  ttrcltr  9698  dmttrcl  9703  frind  9735  kmlem4  10159  ackbij1lem18  10241  infpssr  10313  isf34lem4  10382  fin17  10399  fin67  10400  dffin7-2  10403  fin1a2lem6  10410  axcclem  10462  pwfseqlem3  10672  grothprim  10846  xrlenlt  11301  nzadd  12669  irradd  13026  irrmul  13027  difreicc  13540  fzdif1  13663  modirr  14009  hashinf  14402  sumss  15813  fsumss  15814  prodss  16037  fprodss  16038  fprodn0f  16081  rpnnen2lem12  16316  dvdsaddre2b  16400  sumeven  16480  bitscmp  16531  lcmfunsnlem2  16733  iserodd  16930  prmodvdslcmf  17142  chnccat  18717  symgfix2  19546  pmtrdifellem4  19609  sylow2alem2  19748  efgsfo  19869  gsumval3  20037  gsum2dlem1  20100  gsum2dlem2  20101  ablfac1eu  20205  gsumdixp  20462  isnirred  20564  isirred2  20565  irredn0  20567  0ringdif  20691  0ring1eq0  20698  isdrng3lem2  20918  lsppratlem1  21337  lbsextlem2  21349  xrsmgmdifsgrp  21625  psgnodpm  21804  mplsubrglem  22221  mplcoe1  22256  mplcoe5  22259  opsrtoslem2  22275  selvcllem5  22358  selvvvval  22361  symgmatr01lem  22878  elcls  23301  isclo  23315  maxlp  23375  restntr  23410  isreg2  23605  cmpcld  23630  hausdiag  23874  txkgen  23881  kqcldsat  23962  ufinffr  24158  fin1aufil  24161  alexsublem  24273  alexsubALTlem3  24278  ptcmplem5  24285  blcld  24734  shftmbl  25769  vitalilem4  25842  vitalilem5  25843  vitali  25844  mbfeqalem1  25872  itg1val2  25915  itg10a  25941  itg1ge0a  25942  mbfi1fseqlem4  25949  itg2uba  25974  itg2splitlem  25979  itg2monolem1  25981  itg2cnlem1  25992  itg2cnlem2  25993  itgss  26042  dvtaylp  26609  pserdvlem2  26667  ellogdm  26879  relogbcxp  27025  cxplogb  27026  logbmpt  27028  atandm  27116  atans2  27171  eldmgm  27261  igamgam  27288  igamf  27290  igamcl  27291  lgam1  27303  gam1  27304  wilthlem2  27308  basellem3  27322  fsumvma  27452  dchrelbas2  27476  dchreq  27497  dchrsum  27508  gausslemma2dlem4  27608  2sqreultblem  27687  dchrisum0fno1  27750  rplogsum  27766  newbday  28170  ltslpss  28176  islnopp  29097  frgrncvvdeq  30792  fusgr2wsp2nb  30817  eleigvec  32441  strlem1  32734  strlem5  32739  hstrlem5  32747  difrab2  32976  nfpconfp  33108  fdifsupp  33160  suppiniseg  33161  suppss3  33197  fsuppcurry1  33198  fsuppcurry2  33199  xrdifh  33254  nndiffz1  33260  elrgspnsubrunlem2  33691  ist0cld  34346  ordtconnlem1  34437  esumpinfval  34586  eulerpartlems  34874  eulerpartlemgc  34876  eulerpartlemb  34882  eulerpartlemf  34884  eulerpartlemt  34885  eulerpartlemgh  34892  ballotlemodife  35012  ballotth  35052  reprdifc  35138  hgt750lemb  35167  onvf1od  35707  elmrsubrn  36102  mrsubvrs  36104  dftr6  36333  brsset  36469  dfon3  36472  ellimits  36490  dffun10  36494  elfuns  36495  fullfunfv  36529  dfrecs2  36532  dfrdg4  36533  dfint3  36534  hfext  36766  onsucsuccmpi  37065  bj-rest10b  37842  difunieq  38131  pibt2  38174  iundif1  38356  lindsadd  38370  poimirlem2  38374  poimirlem11  38383  poimirlem12  38384  poimirlem18  38390  poimirlem21  38393  poimirlem22  38394  poimirlem30  38402  itg2addnclem  38423  ftc1anclem5  38449  areacirc  38465  fdc  38498  isfldidl  38821  opelvvdif  39015  iswatN  40870  dochsnkrlem1  42345  unitscyglem4  43067  redvmptabs  43238  fsuppssindlem1  43440  ellz1  43615  pellexlem4  43676  pellexlem5  43677  ordeldif  44102  ordeldifsucon  44103  ordeldif1o  44104  cantnfresb  44168  cantnf2  44169  oadif1lem  44223  oadif1  44224  infordmin  44375  minregex  44377  pwinfig  44404  elnonrel  44428  sqrtcvallem1  44474  clsk3nimkb  44883  ntrclselnel1  44900  ntrneiel2  44929  ntrneik4w  44943  undif3VD  45707  iindif2f  45995  limcrecl  46462  icccncfext  46718  dvmptfprodlem  46775  stoweidlem26  46857  stoweidlem39  46870  stoweidlem52  46883  fourierdlem42  46980  etransclem18  47083  etransclem46  47111  ovolval4lem1  47480  requad01  48540  dfnbgr6  48776  lindslinindsimp1  49390  dignn0fr  49534