Theorem eldif 3900

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 3451	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3451	. . 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 3893	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3624	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

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

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 3432  df-dif 3893

This theorem is referenced by:  eldifd  3901  eldifad  3902  eldifbd  3903  elneeldif  3904  velcomp  3905  difeqri  4069  nfdif  4070  eldifi  4072  eldifn  4073  neldif  4075  difdif  4076  ssconb  4083  sscon  4084  ssdif  4085  raldifb  4090  elsymdif  4199  dfss4  4210  dfun2  4211  dfin2  4212  difin  4213  indifdi  4235  undif3  4241  difin2  4242  ssdif0  4307  difin0ss  4314  inssdif0  4315  reldisj  4394  disj3  4395  undif4  4408  pssnel  4412  inundif  4420  ssundif  4428  eldifpr  4603  elpwunsn  4629  eldiftp  4632  eldifsn  4730  difprsnss  4743  iundif2  5017  iindif1  5018  iindif2  5020  disjss3  5085  brdif  5139  dffr6  5581  difopab  5780  intirr  6076  cnvdif  6102  difxp  6123  xpdifid  6127  frpoind  6301  ordunidif  6368  onmindif  6412  imadif  6577  dffv2  6930  eldifpw  7716  releldmdifi  7992  funeldmdif  7995  xpord2pred  8089  xpord2indlem  8091  ressuppssdif  8129  extmptsuppeq  8132  suppss  8138  suppssr  8139  suppssrg  8140  suppss2  8144  suppofssd  8147  suppcoss  8151  ondif2  8431  oelim2  8525  eldifsucnn  8594  boxcutc  8883  brsdom  8915  brsdom2  9033  php3  9137  unblem1  9196  unfilem1  9209  elfi2  9321  dfsup2  9351  ordtypelem7  9433  ssttrcl  9630  ttrcltr  9631  dmttrcl  9636  frind  9668  kmlem4  10070  ackbij1lem18  10152  infpssr  10224  isf34lem4  10293  fin17  10310  fin67  10311  dffin7-2  10314  fin1a2lem6  10321  axcclem  10373  pwfseqlem3  10577  grothprim  10751  xrlenlt  11204  nzadd  12569  irradd  12917  irrmul  12918  difreicc  13431  fzdif1  13553  modirr  13898  hashinf  14291  sumss  15680  fsumss  15681  prodss  15906  fprodss  15907  fprodn0f  15950  rpnnen2lem12  16186  dvdsaddre2b  16270  sumeven  16350  bitscmp  16401  lcmfunsnlem2  16603  iserodd  16800  prmodvdslcmf  17012  chnccat  18586  symgfix2  19385  pmtrdifellem4  19448  sylow2alem2  19587  efgsfo  19708  gsumval3  19876  gsum2dlem1  19939  gsum2dlem2  19940  ablfac1eu  20044  gsumdixp  20292  isnirred  20394  isirred2  20395  irredn0  20397  0ringdif  20498  0ring1eq0  20504  lsppratlem1  21140  lbsextlem2  21152  xrsmgmdifsgrp  21401  psgnodpm  21581  mplsubrglem  21995  mplcoe1  22028  mplcoe5  22031  opsrtoslem2  22047  symgmatr01lem  22631  elcls  23051  isclo  23065  maxlp  23125  restntr  23160  isreg2  23355  cmpcld  23380  hausdiag  23623  txkgen  23630  kqcldsat  23711  ufinffr  23907  fin1aufil  23910  alexsublem  24022  alexsubALTlem3  24027  ptcmplem5  24034  blcld  24483  shftmbl  25518  vitalilem4  25591  vitalilem5  25592  vitali  25593  mbfeqalem1  25621  itg1val2  25664  itg10a  25690  itg1ge0a  25691  mbfi1fseqlem4  25698  itg2uba  25723  itg2splitlem  25728  itg2monolem1  25730  itg2cnlem1  25741  itg2cnlem2  25742  itgss  25792  dvtaylp  26350  pserdvlem2  26409  ellogdm  26619  relogbcxp  26765  cxplogb  26766  logbmpt  26768  atandm  26856  atans2  26911  eldmgm  27002  igamgam  27029  igamf  27031  igamcl  27032  lgam1  27044  gam1  27045  wilthlem2  27049  basellem3  27063  fsumvma  27193  dchrelbas2  27217  dchreq  27238  dchrsum  27249  gausslemma2dlem4  27349  2sqreultblem  27428  dchrisum0fno1  27491  rplogsum  27507  newbday  27911  ltslpss  27917  islnopp  28824  frgrncvvdeq  30397  fusgr2wsp2nb  30422  eleigvec  32046  strlem1  32339  strlem5  32344  hstrlem5  32352  difrab2  32585  nfpconfp  32723  fdifsupp  32776  suppiniseg  32777  suppss3  32814  fsuppcurry1  32815  fsuppcurry2  32816  xrdifh  32871  nndiffz1  32877  elrgspnsubrunlem2  33327  ist0cld  33996  ordtconnlem1  34087  esumpinfval  34236  eulerpartlems  34523  eulerpartlemgc  34525  eulerpartlemb  34531  eulerpartlemf  34533  eulerpartlemt  34534  eulerpartlemgh  34541  ballotlemodife  34661  ballotth  34701  reprdifc  34790  hgt750lemb  34819  onvf1od  35308  elmrsubrn  35721  mrsubvrs  35723  dftr6  35952  dffr5  35955  brsset  36088  dfon3  36091  ellimits  36109  dffun10  36113  elfuns  36114  fullfunfv  36148  dfrecs2  36151  dfrdg4  36152  dfint3  36153  hfext  36384  onsucsuccmpi  36644  bj-rest10b  37420  difunieq  37707  pibt2  37750  iundif1  37932  lindsadd  37951  poimirlem2  37960  poimirlem11  37969  poimirlem12  37970  poimirlem18  37976  poimirlem21  37979  poimirlem22  37980  poimirlem30  37988  itg2addnclem  38009  ftc1anclem5  38035  areacirc  38051  fdc  38083  isfldidl  38406  opelvvdif  38602  iswatN  40457  dochsnkrlem1  41932  unitscyglem4  42654  redvmptabs  42809  selvcllem5  43032  selvvvval  43035  fsuppssindlem1  43041  ellz1  43216  pellexlem4  43281  pellexlem5  43282  ordeldif  43707  ordeldifsucon  43708  ordeldif1o  43709  cantnfresb  43773  cantnf2  43774  oadif1lem  43828  oadif1  43829  infordmin  43980  minregex  43982  pwinfig  44009  elnonrel  44033  sqrtcvallem1  44079  clsk3nimkb  44488  ntrclselnel1  44505  ntrneiel2  44534  ntrneik4w  44548  undif3VD  45329  iindif2f  45611  limcrecl  46080  icccncfext  46336  dvmptfprodlem  46393  stoweidlem26  46475  stoweidlem39  46488  stoweidlem52  46501  fourierdlem42  46598  etransclem18  46701  etransclem46  46729  ovolval4lem1  47098  nthrucw  47335  requad01  48112  dfnbgr6  48348  lindslinindsimp1  48948  dignn0fr  49092