Theorem eldif 3909

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902

This theorem is used by:  eldifd  3910  eldifad  3911  eldifbd  3912  elneeldif  3913  velcomp  3914  difeqri  4076  nfdif  4077  eldifi  4078  eldifn  4079  neldif  4081  difdif  4082  ssconb  4089  sscon  4090  ssdif  4091  raldifb  4096  elsymdif  4204  dfss4  4215  dfun2  4216  dfin2  4217  difin  4218  indifdi  4240  undif3  4246  difin2  4247  ssdif0  4314  difin0ss  4321  inssdif0OLD  4323  reldisj  4406  disj3  4407  undif4  4420  pssnel  4424  inundif  4435  ssundif  4443  eldifpr  4619  elpwunsn  4645  eldiftp  4648  eldifsn  4748  difprsnss  4762  iundif2  5032  iindif1  5035  iindif2  5037  disjss3  5102  brdif  5158  dffr6  5611  difopab  5811  intirr  6112  cnvdif  6134  difxp  6156  xpdifid  6160  xpdifcnvepel  6161  frpoind  6340  ordunidif  6408  onmindif  6452  imadif  6618  dffv2  6974  eldifpw  7768  releldmdifi  8043  funeldmdif  8046  xpord2pred  8144  xpord2indlem  8146  ressuppssdif  8184  extmptsuppeq  8187  suppss  8193  suppssr  8194  suppssrg  8195  suppss2  8199  suppofssd  8202  suppcoss  8206  ondif2  8490  oelim2  8584  eldifsucnn  8653  boxcutc  8949  brsdom  8981  brsdom2  9100  php3  9204  unblem1  9263  unfilem1  9276  elfi2  9385  dfsup2  9415  ordtypelem7  9497  ssttrcl  9695  ttrcltr  9696  dmttrcl  9701  frind  9733  kmlem4  10157  ackbij1lem18  10239  infpssr  10311  isf34lem4  10380  fin17  10397  fin67  10398  dffin7-2  10401  fin1a2lem6  10408  axcclem  10460  pwfseqlem3  10670  grothprim  10844  xrlenlt  11299  nzadd  12667  irradd  13024  irrmul  13025  difreicc  13538  fzdif1  13661  modirr  14007  hashinf  14400  sumss  15811  fsumss  15812  prodss  16035  fprodss  16036  fprodn0f  16079  rpnnen2lem12  16314  dvdsaddre2b  16398  sumeven  16478  bitscmp  16529  lcmfunsnlem2  16731  iserodd  16928  prmodvdslcmf  17140  chnccat  18715  symgfix2  19544  pmtrdifellem4  19607  sylow2alem2  19746  efgsfo  19867  gsumval3  20035  gsum2dlem1  20098  gsum2dlem2  20099  ablfac1eu  20203  gsumdixp  20460  isnirred  20562  isirred2  20563  irredn0  20565  0ringdif  20689  0ring1eq0  20696  isdrng3lem2  20916  lsppratlem1  21335  lbsextlem2  21347  xrsmgmdifsgrp  21623  psgnodpm  21802  mplsubrglem  22219  mplcoe1  22254  mplcoe5  22257  opsrtoslem2  22273  selvcllem5  22356  selvvvval  22359  symgmatr01lem  22876  elcls  23299  isclo  23313  maxlp  23373  restntr  23408  isreg2  23603  cmpcld  23628  hausdiag  23872  txkgen  23879  kqcldsat  23960  ufinffr  24156  fin1aufil  24159  alexsublem  24271  alexsubALTlem3  24276  ptcmplem5  24283  blcld  24732  shftmbl  25767  vitalilem4  25840  vitalilem5  25841  vitali  25842  mbfeqalem1  25870  itg1val2  25913  itg10a  25939  itg1ge0a  25940  mbfi1fseqlem4  25947  itg2uba  25972  itg2splitlem  25977  itg2monolem1  25979  itg2cnlem1  25990  itg2cnlem2  25991  itgss  26040  dvtaylp  26607  pserdvlem2  26665  ellogdm  26877  relogbcxp  27023  cxplogb  27024  logbmpt  27026  atandm  27114  atans2  27169  eldmgm  27259  igamgam  27286  igamf  27288  igamcl  27289  lgam1  27301  gam1  27302  wilthlem2  27306  basellem3  27320  fsumvma  27450  dchrelbas2  27474  dchreq  27495  dchrsum  27506  gausslemma2dlem4  27606  2sqreultblem  27685  dchrisum0fno1  27748  rplogsum  27764  newbday  28168  ltslpss  28174  islnopp  29095  frgrncvvdeq  30790  fusgr2wsp2nb  30815  eleigvec  32439  strlem1  32732  strlem5  32737  hstrlem5  32745  difrab2  32974  nfpconfp  33106  fdifsupp  33158  suppiniseg  33159  suppss3  33195  fsuppcurry1  33196  fsuppcurry2  33197  xrdifh  33252  nndiffz1  33258  elrgspnsubrunlem2  33689  ist0cld  34344  ordtconnlem1  34435  esumpinfval  34584  eulerpartlems  34872  eulerpartlemgc  34874  eulerpartlemb  34880  eulerpartlemf  34882  eulerpartlemt  34883  eulerpartlemgh  34890  ballotlemodife  35010  ballotth  35050  reprdifc  35136  hgt750lemb  35165  onvf1od  35705  elmrsubrn  36100  mrsubvrs  36102  dftr6  36331  brsset  36467  dfon3  36470  ellimits  36488  dffun10  36492  elfuns  36493  fullfunfv  36527  dfrecs2  36530  dfrdg4  36531  dfint3  36532  hfext  36764  onsucsuccmpi  37063  bj-rest10b  37840  difunieq  38129  pibt2  38172  iundif1  38354  lindsadd  38368  poimirlem2  38372  poimirlem11  38381  poimirlem12  38382  poimirlem18  38388  poimirlem21  38391  poimirlem22  38392  poimirlem30  38400  itg2addnclem  38421  ftc1anclem5  38447  areacirc  38463  fdc  38496  isfldidl  38819  opelvvdif  39013  iswatN  40868  dochsnkrlem1  42343  unitscyglem4  43065  redvmptabs  43236  fsuppssindlem1  43438  ellz1  43613  pellexlem4  43674  pellexlem5  43675  ordeldif  44100  ordeldifsucon  44101  ordeldif1o  44102  cantnfresb  44166  cantnf2  44167  oadif1lem  44221  oadif1  44222  infordmin  44373  minregex  44375  pwinfig  44402  elnonrel  44426  sqrtcvallem1  44472  clsk3nimkb  44881  ntrclselnel1  44898  ntrneiel2  44927  ntrneik4w  44941  undif3VD  45705  iindif2f  45993  limcrecl  46460  icccncfext  46716  dvmptfprodlem  46773  stoweidlem26  46855  stoweidlem39  46868  stoweidlem52  46881  fourierdlem42  46978  etransclem18  47081  etransclem46  47109  ovolval4lem1  47478  requad01  48538  dfnbgr6  48774  lindslinindsimp1  49388  dignn0fr  49532