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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ∖ cdif 3900

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906

This theorem is referenced by:  eldifd  3914  eldifad  3915  eldifbd  3916  elneeldif  3917  velcomp  3918  difeqri  4079  nfdif  4080  eldifi  4082  eldifn  4083  neldif  4085  difdif  4086  ddif  4092  ssconb  4093  sscon  4094  ssdif  4095  raldifb  4100  elsymdif  4209  dfss4  4220  dfun2  4221  dfin2  4222  difin  4223  indifdi  4245  undif3  4251  difin2  4252  ssdif0  4317  difin0ss  4324  inssdif0  4325  reldisj  4404  disj3  4405  undif4  4418  pssnel  4422  inundif  4430  ssundif  4439  eldifpr  4610  elpwunsn  4636  eldiftp  4639  eldifsn  4737  difprsnss  4750  iundif2  5023  iindif1  5024  iindif2  5026  disjss3  5091  brdif  5145  dffr6  5575  difopab  5773  intirr  6067  cnvdif  6092  difxp  6113  xpdifid  6117  frpoind  6290  ordunidif  6357  onmindif  6401  imadif  6566  dffv2  6918  eldifpw  7704  releldmdifi  7980  funeldmdif  7983  xpord2pred  8078  xpord2indlem  8080  ressuppssdif  8118  extmptsuppeq  8121  suppss  8127  suppssr  8128  suppssrg  8129  suppss2  8133  suppofssd  8136  suppcoss  8140  ondif2  8420  oelim2  8513  eldifsucnn  8582  boxcutc  8868  brsdom  8900  brsdom2  9018  php3  9123  unblem1  9181  unfilem1  9194  elfi2  9304  dfsup2  9334  ordtypelem7  9416  ssttrcl  9611  ttrcltr  9612  dmttrcl  9617  frind  9646  kmlem4  10048  ackbij1lem18  10130  infpssr  10202  isf34lem4  10271  fin17  10288  fin67  10289  dffin7-2  10292  fin1a2lem6  10299  axcclem  10351  pwfseqlem3  10554  grothprim  10728  xrlenlt  11180  nzadd  12523  irradd  12874  irrmul  12875  difreicc  13387  fzdif1  13508  modirr  13849  hashinf  14242  sumss  15631  fsumss  15632  prodss  15854  fprodss  15855  fprodn0f  15898  rpnnen2lem12  16134  dvdsaddre2b  16218  sumeven  16298  bitscmp  16349  lcmfunsnlem2  16551  iserodd  16747  prmodvdslcmf  16959  symgfix2  19295  pmtrdifellem4  19358  sylow2alem2  19497  efgsfo  19618  gsumval3  19786  gsum2dlem1  19849  gsum2dlem2  19850  ablfac1eu  19954  gsumdixp  20204  isnirred  20305  isirred2  20306  irredn0  20308  0ringdif  20412  0ring1eq0  20418  lsppratlem1  21054  lbsextlem2  21066  xrsmgmdifsgrp  21315  psgnodpm  21495  mplsubrglem  21911  mplcoe1  21942  mplcoe5  21945  opsrtoslem2  21961  symgmatr01lem  22538  elcls  22958  isclo  22972  maxlp  23032  restntr  23067  isreg2  23262  cmpcld  23287  hausdiag  23530  txkgen  23537  kqcldsat  23618  ufinffr  23814  fin1aufil  23817  alexsublem  23929  alexsubALTlem3  23934  ptcmplem5  23941  blcld  24391  shftmbl  25437  vitalilem4  25510  vitalilem5  25511  vitali  25512  mbfeqalem1  25540  itg1val2  25583  itg10a  25609  itg1ge0a  25610  mbfi1fseqlem4  25617  itg2uba  25642  itg2splitlem  25647  itg2monolem1  25649  itg2cnlem1  25660  itg2cnlem2  25661  itgss  25711  dvtaylp  26276  pserdvlem2  26336  ellogdm  26546  relogbcxp  26693  cxplogb  26694  logbmpt  26696  atandm  26784  atans2  26839  eldmgm  26930  igamgam  26957  igamf  26959  igamcl  26960  lgam1  26972  gam1  26973  wilthlem2  26977  basellem3  26991  fsumvma  27122  dchrelbas2  27146  dchreq  27167  dchrsum  27178  gausslemma2dlem4  27278  2sqreultblem  27357  dchrisum0fno1  27420  rplogsum  27436  newbday  27816  sltlpss  27822  islnopp  28684  frgrncvvdeq  30253  fusgr2wsp2nb  30278  eleigvec  31901  strlem1  32194  strlem5  32199  hstrlem5  32207  difrab2  32442  nfpconfp  32575  fdifsupp  32627  suppiniseg  32628  suppss3  32667  fsuppcurry1  32668  fsuppcurry2  32669  xrdifh  32723  nndiffz1  32729  elrgspnsubrunlem2  33188  ist0cld  33800  ordtconnlem1  33891  esumpinfval  34040  eulerpartlems  34328  eulerpartlemgc  34330  eulerpartlemb  34336  eulerpartlemf  34338  eulerpartlemt  34339  eulerpartlemgh  34346  ballotlemodife  34466  ballotth  34506  reprdifc  34595  hgt750lemb  34624  onvf1od  35084  elmrsubrn  35497  mrsubvrs  35499  dftr6  35728  dffr5  35731  brsset  35867  dfon3  35870  ellimits  35888  dffun10  35892  elfuns  35893  fullfunfv  35925  dfrecs2  35928  dfrdg4  35929  dfint3  35930  hfext  36161  onsucsuccmpi  36421  bj-rest10b  37067  difunieq  37352  pibt2  37395  iundif1  37578  lindsadd  37597  poimirlem2  37606  poimirlem11  37615  poimirlem12  37616  poimirlem18  37622  poimirlem21  37625  poimirlem22  37626  poimirlem30  37634  itg2addnclem  37655  ftc1anclem5  37681  areacirc  37697  fdc  37729  isfldidl  38052  opelvvdif  38238  iswatN  39977  dochsnkrlem1  41452  unitscyglem4  42175  redvmptabs  42337  selvcllem5  42559  selvvvval  42562  fsuppssindlem1  42568  ellz1  42744  pellexlem4  42809  pellexlem5  42810  ordeldif  43235  ordeldifsucon  43236  ordeldif1o  43237  cantnfresb  43301  cantnf2  43302  oadif1lem  43356  oadif1  43357  infordmin  43509  minregex  43511  pwinfig  43538  elnonrel  43562  sqrtcvallem1  43608  clsk3nimkb  44017  ntrclselnel1  44034  ntrneiel2  44063  ntrneik4w  44077  undif3VD  44859  iindif2f  45142  limcrecl  45614  icccncfext  45872  dvmptfprodlem  45929  stoweidlem26  46011  stoweidlem39  46024  stoweidlem52  46037  fourierdlem42  46134  etransclem18  46237  etransclem46  46265  ovolval4lem1  46634  requad01  47609  dfnbgr6  47845  lindslinindsimp1  48446  dignn0fr  48590