Theorem eldif 3550

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 3185	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3185	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2676	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2676	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 307	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 743	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3543	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3322	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 367	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ∖ cdif 3537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543

This theorem is referenced by:  eldifd  3551  eldifad  3552  eldifbd  3553  difeqri  3692  eldifi  3694  eldifn  3695  neldif  3697  difdif  3698  ddif  3704  ssconb  3705  sscon  3706  ssdif  3707  raldifb  3712  elsymdif  3811  symdif2  3814  dfss4  3820  dfun2  3821  dfin2  3822  difin  3823  indifdir  3842  undif3  3847  undif3OLD  3848  difin2  3849  dfnul2  3876  ssdif0  3896  difin0ss  3900  inssdif0  3901  reldisj  3972  disj3  3973  undif4  3987  pssnel  3991  inundif  3998  ssundif  4004  eldifpr  4152  elpwunsn  4171  eldiftp  4175  eldifsn  4260  difprsnss  4270  iundif2  4523  iindif2  4525  disjss3  4582  brdif  4635  difopab  5175  intirr  5433  cnvdif  5458  difxp  5477  xpdifid  5481  wfi  5630  ordunidif  5690  onmindif  5732  imadif  5887  dffv2  6181  eldifpw  6868  ressuppssdif  7203  extmptsuppeq  7206  suppss  7212  suppssr  7213  suppss2  7216  ondif2  7469  oelim2  7562  boxcutc  7837  brsdom  7864  brsdom2  7969  php3  8031  unblem1  8097  unfilem1  8109  elfi2  8203  dfsup2  8233  ordtypelem7  8312  kmlem4  8858  ackbij1lem18  8942  infpssr  9013  isf34lem4  9082  fin17  9099  fin67  9100  dffin7-2  9103  fin1a2lem6  9110  axcclem  9162  pwfseqlem3  9361  grothprim  9535  xrlenlt  9982  nzadd  11302  irradd  11688  irrmul  11689  difreicc  12175  modirr  12603  hashinf  12984  sumss  14302  fsumss  14303  prodss  14516  fprodss  14517  fprodn0f  14561  rpnnen2lem12  14793  dvdsaddre2b  14867  sumeven  14948  bitscmp  14998  lcmfunsnlem2  15191  iserodd  15378  prmodvdslcmf  15589  symgfix2  17659  pmtrdifellem4  17722  sylow2alem2  17856  efgsfo  17975  gsumval3  18131  gsum2dlem1  18192  gsum2dlem2  18193  ablfac1eu  18295  gsumdixp  18432  isnirred  18523  isirred2  18524  irredn0  18526  lsppratlem1  18968  lbsextlem2  18980  mplsubrglem  19260  mplcoe1  19286  mplcoe5  19289  opsrtoslem2  19306  xrsmgmdifsgrp  19602  psgnodpm  19753  symgmatr01lem  20278  elcls  20687  isclo  20701  maxlp  20761  restntr  20796  isreg2  20991  cmpcld  21015  hausdiag  21258  txkgen  21265  kqcldsat  21346  ufinffr  21543  fin1aufil  21546  alexsublem  21658  alexsubALTlem3  21663  ptcmplem5  21670  blcld  22120  shftmbl  23113  vitalilem4  23186  vitalilem5  23187  vitali  23188  mbfeqalem  23215  itg1val2  23257  itg10a  23283  itg1ge0a  23284  mbfi1fseqlem4  23291  itg2uba  23316  itg2splitlem  23321  itg2monolem1  23323  itg2cnlem1  23334  itg2cnlem2  23335  itgss  23384  dvtaylp  23928  pserdvlem2  23986  ellogdm  24185  relogbcxp  24323  cxplogb  24324  logbmpt  24326  atandm  24403  atans2  24458  eldmgm  24548  igamgam  24575  igamf  24577  igamcl  24578  lgam1  24590  gam1  24591  wilthlem2  24595  basellem3  24609  fsumvma  24738  dchrelbas2  24762  dchreq  24783  dchrsum  24794  gausslemma2dlem4  24894  dchrisum0fno1  25000  rplogsum  25016  islnopp  25431  isusgra0  25876  usgraop  25879  nbcusgra  25992  frgraunss  26522  frgrancvvdeqlem3  26559  frgrancvvdeqlem9  26568  frgrawopreglem3  26573  frgrawopreglem4  26574  frgrawopreg  26576  usg2spot2nb  26592  eleigvec  28200  strlem1  28493  strlem5  28498  hstrlem5  28506  suppss3  28890  xrdifh  28932  nndiffz1  28936  ordtconlem1  29298  esumpinfval  29462  eulerpartlems  29749  eulerpartlemgc  29751  eulerpartlemb  29757  eulerpartlemf  29759  eulerpartlemt  29760  eulerpartlemgh  29767  ballotlemodife  29886  ballotth  29926  elmrsubrn  30671  mrsubvrs  30673  dftr6  30893  dffr5  30896  frind  30984  brsset  31166  dfon3  31169  ellimits  31187  dffun10  31191  elfuns  31192  fullfunfv  31224  dfrecs2  31227  dfrdg4  31228  dfint3  31229  hfext  31460  onsucsuccmpi  31612  bj-rest10b  32223  iundif1  32553  poimirlem2  32581  poimirlem11  32590  poimirlem12  32591  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  poimirlem30  32609  itg2addnclem  32631  ftc1anclem5  32659  areacirc  32675  fdc  32711  isfldidl  33037  iswatN  34298  dochsnkrlem1  35776  ellz1  36348  pellexlem4  36414  pellexlem5  36415  pwinfig  36885  elnonrel  36910  clsk3nimkb  37358  ntrclselnel1  37375  ntrneiel2  37404  ntrneik4w  37418  compel  37663  undif3VD  38140  limcrecl  38696  icccncfext  38773  dvmptfprodlem  38834  stoweidlem26  38919  stoweidlem39  38932  stoweidlem52  38945  fourierdlem42  39042  etransclem18  39145  etransclem46  39173  ovolval4lem1  39539  frgrncvvdeqlem3  41471  frgrncvvdeq  41480  frgrwopreglem3  41483  frgrwopreglem4  41484  frgrwopreg  41486  fusgr2wsp2nb  41498  0ringdif  41660  0ring1eq0  41662  lindslinindsimp1  42040  dignn0fr  42193