Theorem eldif 3916

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 3478	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3478	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2853	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2853	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3909	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3641	. 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 2146  Vcvv 3457   ∖ cdif 3903

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909

This theorem is used by:  eldifd  3917  eldifad  3918  eldifbd  3919  elneeldif  3920  velcomp  3921  difeqri  4083  nfdif  4084  eldifi  4085  eldifn  4086  neldif  4088  difdif  4089  ssconb  4096  sscon  4097  ssdif  4098  raldifb  4103  elsymdif  4211  dfss4  4222  dfun2  4223  dfin2  4224  difin  4225  indifdi  4247  undif3  4253  difin2  4254  ssdif0  4321  difin0ss  4328  inssdif0OLD  4330  reldisj  4413  disj3  4414  undif4  4427  pssnel  4431  inundif  4442  ssundif  4450  eldifpr  4626  elpwunsn  4652  eldiftp  4655  eldifsn  4755  difprsnss  4769  iundif2  5040  iindif1  5043  iindif2  5045  disjss3  5110  brdif  5166  dffr6  5619  difopab  5819  intirr  6120  cnvdif  6142  difxp  6163  xpdifid  6167  xpdifcnvepel  6168  frpoind  6347  ordunidif  6415  onmindif  6459  imadif  6624  dffv2  6980  eldifpw  7773  releldmdifi  8048  funeldmdif  8051  xpord2pred  8147  xpord2indlem  8149  ressuppssdif  8187  extmptsuppeq  8190  suppss  8196  suppssr  8197  suppssrg  8198  suppss2  8202  suppofssd  8205  suppcoss  8209  ondif2  8493  oelim2  8587  eldifsucnn  8656  boxcutc  8945  brsdom  8977  brsdom2  9096  php3  9200  unblem1  9259  unfilem1  9272  elfi2  9381  dfsup2  9411  ordtypelem7  9493  ssttrcl  9691  ttrcltr  9692  dmttrcl  9697  frind  9729  kmlem4  10153  ackbij1lem18  10235  infpssr  10307  isf34lem4  10376  fin17  10393  fin67  10394  dffin7-2  10397  fin1a2lem6  10404  axcclem  10456  pwfseqlem3  10662  grothprim  10836  xrlenlt  11291  nzadd  12659  irradd  13015  irrmul  13016  difreicc  13529  fzdif1  13652  modirr  13998  hashinf  14391  sumss  15800  fsumss  15801  prodss  16026  fprodss  16027  fprodn0f  16070  rpnnen2lem12  16305  dvdsaddre2b  16389  sumeven  16469  bitscmp  16520  lcmfunsnlem2  16722  iserodd  16919  prmodvdslcmf  17131  chnccat  18706  symgfix2  19532  pmtrdifellem4  19595  sylow2alem2  19734  efgsfo  19855  gsumval3  20023  gsum2dlem1  20086  gsum2dlem2  20087  ablfac1eu  20191  gsumdixp  20448  isnirred  20550  isirred2  20551  irredn0  20553  0ringdif  20677  0ring1eq0  20684  isdrng3lem2  20904  lsppratlem1  21323  lbsextlem2  21335  xrsmgmdifsgrp  21611  psgnodpm  21790  mplsubrglem  22205  mplcoe1  22240  mplcoe5  22243  opsrtoslem2  22259  selvcllem5  22342  selvvvval  22345  symgmatr01lem  22862  elcls  23282  isclo  23296  maxlp  23356  restntr  23391  isreg2  23586  cmpcld  23611  hausdiag  23855  txkgen  23862  kqcldsat  23943  ufinffr  24139  fin1aufil  24142  alexsublem  24254  alexsubALTlem3  24259  ptcmplem5  24266  blcld  24715  shftmbl  25750  vitalilem4  25823  vitalilem5  25824  vitali  25825  mbfeqalem1  25853  itg1val2  25896  itg10a  25922  itg1ge0a  25923  mbfi1fseqlem4  25930  itg2uba  25955  itg2splitlem  25960  itg2monolem1  25962  itg2cnlem1  25973  itg2cnlem2  25974  itgss  26024  dvtaylp  26586  pserdvlem2  26644  ellogdm  26857  relogbcxp  27003  cxplogb  27004  logbmpt  27006  atandm  27094  atans2  27149  eldmgm  27239  igamgam  27266  igamf  27268  igamcl  27269  lgam1  27281  gam1  27282  wilthlem2  27286  basellem3  27300  fsumvma  27430  dchrelbas2  27454  dchreq  27475  dchrsum  27486  gausslemma2dlem4  27586  2sqreultblem  27665  dchrisum0fno1  27728  rplogsum  27744  newbday  28148  ltslpss  28154  islnopp  29073  frgrncvvdeq  30733  fusgr2wsp2nb  30758  eleigvec  32382  strlem1  32675  strlem5  32680  hstrlem5  32688  difrab2  32917  nfpconfp  33050  fdifsupp  33103  suppiniseg  33104  suppss3  33140  fsuppcurry1  33141  fsuppcurry2  33142  xrdifh  33197  nndiffz1  33203  elrgspnsubrunlem2  33634  ist0cld  34289  ordtconnlem1  34380  esumpinfval  34529  eulerpartlems  34817  eulerpartlemgc  34819  eulerpartlemb  34825  eulerpartlemf  34827  eulerpartlemt  34828  eulerpartlemgh  34835  ballotlemodife  34955  ballotth  34995  reprdifc  35081  hgt750lemb  35110  onvf1od  35650  elmrsubrn  36051  mrsubvrs  36053  dftr6  36282  dffr5  36285  brsset  36418  dfon3  36421  ellimits  36439  dffun10  36443  elfuns  36444  fullfunfv  36478  dfrecs2  36481  dfrdg4  36482  dfint3  36483  hfext  36714  onsucsuccmpi  37013  bj-rest10b  37790  difunieq  38079  pibt2  38122  iundif1  38304  lindsadd  38323  poimirlem2  38332  poimirlem11  38341  poimirlem12  38342  poimirlem18  38348  poimirlem21  38351  poimirlem22  38352  poimirlem30  38360  itg2addnclem  38381  ftc1anclem5  38407  areacirc  38423  fdc  38456  isfldidl  38779  opelvvdif  38973  iswatN  40828  dochsnkrlem1  42303  unitscyglem4  43025  redvmptabs  43181  fsuppssindlem1  43383  ellz1  43558  pellexlem4  43619  pellexlem5  43620  ordeldif  44045  ordeldifsucon  44046  ordeldif1o  44047  cantnfresb  44111  cantnf2  44112  oadif1lem  44166  oadif1  44167  infordmin  44318  minregex  44320  pwinfig  44347  elnonrel  44371  sqrtcvallem1  44417  clsk3nimkb  44826  ntrclselnel1  44843  ntrneiel2  44872  ntrneik4w  44886  undif3VD  45650  iindif2f  45938  limcrecl  46405  icccncfext  46661  dvmptfprodlem  46718  stoweidlem26  46800  stoweidlem39  46813  stoweidlem52  46826  fourierdlem42  46923  etransclem18  47026  etransclem46  47054  ovolval4lem1  47423  requad01  48446  dfnbgr6  48682  lindslinindsimp1  49296  dignn0fr  49440