Theorem eldif 3913

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906

This theorem is referenced by:  eldifd  3914  eldifad  3915  eldifbd  3916  elneeldif  3917  velcomp  3918  difeqri  4082  nfdif  4083  eldifi  4085  eldifn  4086  neldif  4088  difdif  4089  ddif  4095  ssconb  4096  sscon  4097  ssdif  4098  raldifb  4103  elsymdif  4212  dfss4  4223  dfun2  4224  dfin2  4225  difin  4226  indifdi  4248  undif3  4254  difin2  4255  ssdif0  4320  difin0ss  4327  inssdif0  4328  reldisj  4407  disj3  4408  undif4  4421  pssnel  4425  inundif  4433  ssundif  4442  eldifpr  4617  elpwunsn  4643  eldiftp  4646  eldifsn  4744  difprsnss  4757  iundif2  5031  iindif1  5032  iindif2  5034  disjss3  5099  brdif  5153  dffr6  5588  difopab  5787  intirr  6083  cnvdif  6109  difxp  6130  xpdifid  6134  frpoind  6308  ordunidif  6375  onmindif  6419  imadif  6584  dffv2  6937  eldifpw  7723  releldmdifi  7999  funeldmdif  8002  xpord2pred  8097  xpord2indlem  8099  ressuppssdif  8137  extmptsuppeq  8140  suppss  8146  suppssr  8147  suppssrg  8148  suppss2  8152  suppofssd  8155  suppcoss  8159  ondif2  8439  oelim2  8533  eldifsucnn  8602  boxcutc  8891  brsdom  8923  brsdom2  9041  php3  9145  unblem1  9204  unfilem1  9217  elfi2  9329  dfsup2  9359  ordtypelem7  9441  ssttrcl  9636  ttrcltr  9637  dmttrcl  9642  frind  9674  kmlem4  10076  ackbij1lem18  10158  infpssr  10230  isf34lem4  10299  fin17  10316  fin67  10317  dffin7-2  10320  fin1a2lem6  10327  axcclem  10379  pwfseqlem3  10583  grothprim  10757  xrlenlt  11209  nzadd  12551  irradd  12898  irrmul  12899  difreicc  13412  fzdif1  13533  modirr  13877  hashinf  14270  sumss  15659  fsumss  15660  prodss  15882  fprodss  15883  fprodn0f  15926  rpnnen2lem12  16162  dvdsaddre2b  16246  sumeven  16326  bitscmp  16377  lcmfunsnlem2  16579  iserodd  16775  prmodvdslcmf  16987  chnccat  18561  symgfix2  19357  pmtrdifellem4  19420  sylow2alem2  19559  efgsfo  19680  gsumval3  19848  gsum2dlem1  19911  gsum2dlem2  19912  ablfac1eu  20016  gsumdixp  20266  isnirred  20368  isirred2  20369  irredn0  20371  0ringdif  20472  0ring1eq0  20478  lsppratlem1  21114  lbsextlem2  21126  xrsmgmdifsgrp  21375  psgnodpm  21555  mplsubrglem  21971  mplcoe1  22004  mplcoe5  22007  opsrtoslem2  22023  symgmatr01lem  22609  elcls  23029  isclo  23043  maxlp  23103  restntr  23138  isreg2  23333  cmpcld  23358  hausdiag  23601  txkgen  23608  kqcldsat  23689  ufinffr  23885  fin1aufil  23888  alexsublem  24000  alexsubALTlem3  24005  ptcmplem5  24012  blcld  24461  shftmbl  25507  vitalilem4  25580  vitalilem5  25581  vitali  25582  mbfeqalem1  25610  itg1val2  25653  itg10a  25679  itg1ge0a  25680  mbfi1fseqlem4  25687  itg2uba  25712  itg2splitlem  25717  itg2monolem1  25719  itg2cnlem1  25730  itg2cnlem2  25731  itgss  25781  dvtaylp  26346  pserdvlem2  26406  ellogdm  26616  relogbcxp  26763  cxplogb  26764  logbmpt  26766  atandm  26854  atans2  26909  eldmgm  27000  igamgam  27027  igamf  27029  igamcl  27030  lgam1  27042  gam1  27043  wilthlem2  27047  basellem3  27061  fsumvma  27192  dchrelbas2  27216  dchreq  27237  dchrsum  27248  gausslemma2dlem4  27348  2sqreultblem  27427  dchrisum0fno1  27490  rplogsum  27506  newbday  27910  ltslpss  27916  islnopp  28823  frgrncvvdeq  30396  fusgr2wsp2nb  30421  eleigvec  32045  strlem1  32338  strlem5  32343  hstrlem5  32351  difrab2  32584  nfpconfp  32722  fdifsupp  32775  suppiniseg  32776  suppss3  32813  fsuppcurry1  32814  fsuppcurry2  32815  xrdifh  32871  nndiffz1  32877  elrgspnsubrunlem2  33342  ist0cld  34011  ordtconnlem1  34102  esumpinfval  34251  eulerpartlems  34538  eulerpartlemgc  34540  eulerpartlemb  34546  eulerpartlemf  34548  eulerpartlemt  34549  eulerpartlemgh  34556  ballotlemodife  34676  ballotth  34716  reprdifc  34805  hgt750lemb  34834  onvf1od  35323  elmrsubrn  35736  mrsubvrs  35738  dftr6  35967  dffr5  35970  brsset  36103  dfon3  36106  ellimits  36124  dffun10  36128  elfuns  36129  fullfunfv  36163  dfrecs2  36166  dfrdg4  36167  dfint3  36168  hfext  36399  onsucsuccmpi  36659  bj-rest10b  37342  difunieq  37629  pibt2  37672  iundif1  37845  lindsadd  37864  poimirlem2  37873  poimirlem11  37882  poimirlem12  37883  poimirlem18  37889  poimirlem21  37892  poimirlem22  37893  poimirlem30  37901  itg2addnclem  37922  ftc1anclem5  37948  areacirc  37964  fdc  37996  isfldidl  38319  opelvvdif  38515  iswatN  40370  dochsnkrlem1  41845  unitscyglem4  42568  redvmptabs  42730  selvcllem5  42940  selvvvval  42943  fsuppssindlem1  42949  ellz1  43124  pellexlem4  43189  pellexlem5  43190  ordeldif  43615  ordeldifsucon  43616  ordeldif1o  43617  cantnfresb  43681  cantnf2  43682  oadif1lem  43736  oadif1  43737  infordmin  43888  minregex  43890  pwinfig  43917  elnonrel  43941  sqrtcvallem1  43987  clsk3nimkb  44396  ntrclselnel1  44413  ntrneiel2  44442  ntrneik4w  44456  undif3VD  45237  iindif2f  45519  limcrecl  45989  icccncfext  46245  dvmptfprodlem  46302  stoweidlem26  46384  stoweidlem39  46397  stoweidlem52  46410  fourierdlem42  46507  etransclem18  46610  etransclem46  46638  ovolval4lem1  47007  nthrucw  47244  requad01  47981  dfnbgr6  48217  lindslinindsimp1  48817  dignn0fr  48961