Theorem eldif 3915

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 3476	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3476	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 485	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2851	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2851	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 643	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3908	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3639	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908

This theorem is referenced by:  eldifd  3916  eldifad  3917  eldifbd  3918  elneeldif  3919  velcomp  3920  difeqri  4083  nfdif  4084  eldifi  4085  eldifn  4086  neldif  4088  difdif  4089  ssconb  4096  sscon  4097  ssdif  4098  raldifb  4103  elsymdif  4211  dfss4  4222  dfun2  4223  dfin2  4224  difin  4225  indifdi  4247  undif3  4253  difin2  4254  ssdif0  4321  difin0ss  4328  inssdif0OLD  4330  reldisj  4413  disj3  4414  undif4  4427  pssnel  4431  inundif  4440  ssundif  4448  eldifpr  4624  elpwunsn  4650  eldiftp  4653  eldifsn  4753  difprsnss  4767  iundif2  5038  iindif1  5041  iindif2  5043  disjss3  5108  brdif  5164  dffr6  5617  difopab  5817  intirr  6118  cnvdif  6140  difxp  6161  xpdifid  6165  xpdifcnvepel  6166  frpoind  6343  ordunidif  6411  onmindif  6455  imadif  6620  dffv2  6976  eldifpw  7763  releldmdifi  8038  funeldmdif  8041  xpord2pred  8137  xpord2indlem  8139  ressuppssdif  8177  extmptsuppeq  8180  suppss  8186  suppssr  8187  suppssrg  8188  suppss2  8192  suppofssd  8195  suppcoss  8199  ondif2  8483  oelim2  8577  eldifsucnn  8646  boxcutc  8935  brsdom  8967  brsdom2  9085  php3  9189  unblem1  9248  unfilem1  9261  elfi2  9370  dfsup2  9400  ordtypelem7  9482  ssttrcl  9680  ttrcltr  9681  dmttrcl  9686  frind  9718  kmlem4  10133  ackbij1lem18  10215  infpssr  10287  isf34lem4  10356  fin17  10373  fin67  10374  dffin7-2  10377  fin1a2lem6  10384  axcclem  10436  pwfseqlem3  10640  grothprim  10814  xrlenlt  11269  nzadd  12637  irradd  12992  irrmul  12993  difreicc  13506  fzdif1  13629  modirr  13974  hashinf  14367  sumss  15771  fsumss  15772  prodss  15997  fprodss  15998  fprodn0f  16041  rpnnen2lem12  16276  dvdsaddre2b  16360  sumeven  16440  bitscmp  16491  lcmfunsnlem2  16693  iserodd  16890  prmodvdslcmf  17102  chnccat  18677  symgfix2  19481  pmtrdifellem4  19544  sylow2alem2  19683  efgsfo  19804  gsumval3  19972  gsum2dlem1  20035  gsum2dlem2  20036  ablfac1eu  20140  gsumdixp  20396  isnirred  20498  isirred2  20499  irredn0  20501  0ringdif  20625  0ring1eq0  20632  isdrng3lem2  20852  lsppratlem1  21271  lbsextlem2  21283  xrsmgmdifsgrp  21559  psgnodpm  21738  mplsubrglem  22153  mplcoe1  22188  mplcoe5  22191  opsrtoslem2  22207  selvcllem5  22290  selvvvval  22293  symgmatr01lem  22810  elcls  23230  isclo  23244  maxlp  23304  restntr  23339  isreg2  23534  cmpcld  23559  hausdiag  23802  txkgen  23809  kqcldsat  23890  ufinffr  24086  fin1aufil  24089  alexsublem  24201  alexsubALTlem3  24206  ptcmplem5  24213  blcld  24662  shftmbl  25697  vitalilem4  25770  vitalilem5  25771  vitali  25772  mbfeqalem1  25800  itg1val2  25843  itg10a  25869  itg1ge0a  25870  mbfi1fseqlem4  25877  itg2uba  25902  itg2splitlem  25907  itg2monolem1  25909  itg2cnlem1  25920  itg2cnlem2  25921  itgss  25971  dvtaylp  26533  pserdvlem2  26591  ellogdm  26804  relogbcxp  26950  cxplogb  26951  logbmpt  26953  atandm  27041  atans2  27096  eldmgm  27186  igamgam  27213  igamf  27215  igamcl  27216  lgam1  27228  gam1  27229  wilthlem2  27233  basellem3  27247  fsumvma  27377  dchrelbas2  27401  dchreq  27422  dchrsum  27433  gausslemma2dlem4  27533  2sqreultblem  27612  dchrisum0fno1  27675  rplogsum  27691  newbday  28095  ltslpss  28101  islnopp  29020  frgrncvvdeq  30660  fusgr2wsp2nb  30685  eleigvec  32309  strlem1  32602  strlem5  32607  hstrlem5  32615  difrab2  32844  nfpconfp  32977  fdifsupp  33030  suppiniseg  33031  suppss3  33068  fsuppcurry1  33069  fsuppcurry2  33070  xrdifh  33125  nndiffz1  33131  elrgspnsubrunlem2  33568  ist0cld  34223  ordtconnlem1  34314  esumpinfval  34463  eulerpartlems  34750  eulerpartlemgc  34752  eulerpartlemb  34758  eulerpartlemf  34760  eulerpartlemt  34761  eulerpartlemgh  34768  ballotlemodife  34888  ballotth  34928  reprdifc  35014  hgt750lemb  35043  onvf1od  35591  elmrsubrn  36012  mrsubvrs  36014  dftr6  36243  dffr5  36246  brsset  36379  dfon3  36382  ellimits  36400  dffun10  36404  elfuns  36405  fullfunfv  36439  dfrecs2  36442  dfrdg4  36443  dfint3  36444  hfext  36675  onsucsuccmpi  36974  bj-rest10b  37751  difunieq  38040  pibt2  38083  iundif1  38265  lindsadd  38284  poimirlem2  38293  poimirlem11  38302  poimirlem12  38303  poimirlem18  38309  poimirlem21  38312  poimirlem22  38313  poimirlem30  38321  itg2addnclem  38342  ftc1anclem5  38368  areacirc  38384  fdc  38416  isfldidl  38739  opelvvdif  38933  iswatN  40788  dochsnkrlem1  42263  unitscyglem4  42985  redvmptabs  43141  fsuppssindlem1  43343  ellz1  43518  pellexlem4  43579  pellexlem5  43580  ordeldif  44005  ordeldifsucon  44006  ordeldif1o  44007  cantnfresb  44071  cantnf2  44072  oadif1lem  44126  oadif1  44127  infordmin  44278  minregex  44280  pwinfig  44307  elnonrel  44331  sqrtcvallem1  44377  clsk3nimkb  44786  ntrclselnel1  44803  ntrneiel2  44832  ntrneik4w  44846  undif3VD  45610  iindif2f  45898  limcrecl  46365  icccncfext  46621  dvmptfprodlem  46678  stoweidlem26  46760  stoweidlem39  46773  stoweidlem52  46786  fourierdlem42  46883  etransclem18  46986  etransclem46  47014  ovolval4lem1  47383  requad01  48406  dfnbgr6  48642  lindslinindsimp1  49257  dignn0fr  49401