Theorem eldif 3958

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ∖ cdif 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3951

This theorem is referenced by:  eldifd  3959  eldifad  3960  eldifbd  3961  elneeldif  3962  velcomp  3963  difeqri  4124  eldifi  4126  eldifn  4127  neldif  4129  difdif  4130  ddif  4136  ssconb  4137  sscon  4138  ssdif  4139  raldifb  4144  elsymdif  4247  dfss4  4258  dfun2  4259  dfin2  4260  difin  4261  indifdi  4283  indifdirOLD  4285  undif3  4290  difin2  4291  ssdif0  4363  difin0ss  4368  inssdif0  4369  reldisj  4451  reldisjOLD  4452  disj3  4453  undif4  4466  pssnel  4470  inundif  4478  ssundif  4487  eldifpr  4660  elpwunsn  4687  eldiftp  4690  eldifsn  4790  difprsnss  4802  iundif2  5077  iindif1  5078  iindif2  5080  disjss3  5147  brdif  5201  dffr6  5634  difopab  5829  difopabOLD  5830  intirr  6117  cnvdif  6141  difxp  6161  xpdifid  6165  frpoind  6341  wfiOLD  6350  ordunidif  6411  onmindif  6454  imadif  6630  dffv2  6984  eldifpw  7752  releldmdifi  8028  funeldmdif  8031  xpord2pred  8128  xpord2indlem  8130  ressuppssdif  8167  extmptsuppeq  8170  suppss  8176  suppssOLD  8177  suppssr  8178  suppssrg  8179  suppss2  8182  suppofssd  8185  suppcoss  8189  ondif2  8499  oelim2  8592  eldifsucnn  8660  boxcutc  8932  brsdom  8968  brsdom2  9094  php3  9209  php3OLD  9221  unblem1  9292  unfilem1  9307  elfi2  9406  dfsup2  9436  ordtypelem7  9516  ssttrcl  9707  ttrcltr  9708  dmttrcl  9713  frind  9742  kmlem4  10145  ackbij1lem18  10229  infpssr  10300  isf34lem4  10369  fin17  10386  fin67  10387  dffin7-2  10390  fin1a2lem6  10397  axcclem  10449  pwfseqlem3  10652  grothprim  10826  xrlenlt  11276  nzadd  12607  irradd  12954  irrmul  12955  difreicc  13458  modirr  13904  hashinf  14292  sumss  15667  fsumss  15668  prodss  15888  fprodss  15889  fprodn0f  15932  rpnnen2lem12  16165  dvdsaddre2b  16247  sumeven  16327  bitscmp  16376  lcmfunsnlem2  16574  iserodd  16765  prmodvdslcmf  16977  symgfix2  19279  pmtrdifellem4  19342  sylow2alem2  19481  efgsfo  19602  gsumval3  19770  gsum2dlem1  19833  gsum2dlem2  19834  ablfac1eu  19938  gsumdixp  20125  isnirred  20227  isirred2  20228  irredn0  20230  lsppratlem1  20753  lbsextlem2  20765  xrsmgmdifsgrp  20975  psgnodpm  21133  mplsubrglem  21555  mplcoe1  21584  mplcoe5  21587  opsrtoslem2  21609  symgmatr01lem  22147  elcls  22569  isclo  22583  maxlp  22643  restntr  22678  isreg2  22873  cmpcld  22898  hausdiag  23141  txkgen  23148  kqcldsat  23229  ufinffr  23425  fin1aufil  23428  alexsublem  23540  alexsubALTlem3  23545  ptcmplem5  23552  blcld  24006  shftmbl  25047  vitalilem4  25120  vitalilem5  25121  vitali  25122  mbfeqalem1  25150  itg1val2  25193  itg10a  25220  itg1ge0a  25221  mbfi1fseqlem4  25228  itg2uba  25253  itg2splitlem  25258  itg2monolem1  25260  itg2cnlem1  25271  itg2cnlem2  25272  itgss  25321  dvtaylp  25874  pserdvlem2  25932  ellogdm  26139  relogbcxp  26280  cxplogb  26281  logbmpt  26283  atandm  26371  atans2  26426  eldmgm  26516  igamgam  26543  igamf  26545  igamcl  26546  lgam1  26558  gam1  26559  wilthlem2  26563  basellem3  26577  fsumvma  26706  dchrelbas2  26730  dchreq  26751  dchrsum  26762  gausslemma2dlem4  26862  2sqreultblem  26941  dchrisum0fno1  27004  rplogsum  27020  newbday  27386  sltlpss  27391  islnopp  27980  frgrncvvdeq  29552  fusgr2wsp2nb  29577  eleigvec  31198  strlem1  31491  strlem5  31496  hstrlem5  31504  difrab2  31726  nfpconfp  31844  suppiniseg  31896  suppss3  31937  fsuppcurry1  31938  fsuppcurry2  31939  xrdifh  31979  nndiffz1  31985  ist0cld  32802  ordtconnlem1  32893  esumpinfval  33060  eulerpartlems  33348  eulerpartlemgc  33350  eulerpartlemb  33356  eulerpartlemf  33358  eulerpartlemt  33359  eulerpartlemgh  33366  ballotlemodife  33485  ballotth  33525  reprdifc  33628  hgt750lemb  33657  elmrsubrn  34500  mrsubvrs  34502  dftr6  34710  dffr5  34713  brsset  34850  dfon3  34853  ellimits  34871  dffun10  34875  elfuns  34876  fullfunfv  34908  dfrecs2  34911  dfrdg4  34912  dfint3  34913  hfext  35144  onsucsuccmpi  35317  bj-rest10b  35959  difunieq  36244  pibt2  36287  iundif1  36451  lindsadd  36470  poimirlem2  36479  poimirlem11  36488  poimirlem12  36489  poimirlem18  36495  poimirlem21  36498  poimirlem22  36499  poimirlem30  36507  itg2addnclem  36528  ftc1anclem5  36554  areacirc  36570  fdc  36602  isfldidl  36925  opelvvdif  37116  iswatN  38854  dochsnkrlem1  40329  selvcllem5  41152  selvvvval  41155  fsuppssindlem1  41161  ellz1  41491  pellexlem4  41556  pellexlem5  41557  ordeldif  41994  ordeldifsucon  41995  ordeldif1o  41996  cantnfresb  42060  cantnf2  42061  oadif1lem  42115  oadif1  42116  infordmin  42269  minregex  42271  pwinfig  42298  elnonrel  42322  sqrtcvallem1  42368  clsk3nimkb  42777  ntrclselnel1  42794  ntrneiel2  42823  ntrneik4w  42837  undif3VD  43629  iindif2f  43840  limcrecl  44332  icccncfext  44590  dvmptfprodlem  44647  stoweidlem26  44729  stoweidlem39  44742  stoweidlem52  44755  fourierdlem42  44852  etransclem18  44955  etransclem46  44983  ovolval4lem1  45352  requad01  46276  0ringdif  46631  0ring1eq0  46633  lindslinindsimp1  47092  dignn0fr  47241