Theorem eldif 3908

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 3459	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2824	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2824	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 317	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 631	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3901	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3621	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 379	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  Vcvv 3441   ∖ cdif 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-dif 3901

This theorem is referenced by:  eldifd  3909  eldifad  3910  eldifbd  3911  elneeldif  3912  velcomp  3913  difeqri  4072  eldifi  4074  eldifn  4075  neldif  4077  difdif  4078  ddif  4084  ssconb  4085  sscon  4086  ssdif  4087  raldifb  4092  elsymdif  4195  dfss4  4206  dfun2  4207  dfin2  4208  difin  4209  indifdi  4231  indifdirOLD  4233  undif3  4238  difin2  4239  ssdif0  4311  difin0ss  4316  inssdif0  4317  reldisj  4399  reldisjOLD  4400  disj3  4401  undif4  4414  pssnel  4418  inundif  4426  ssundif  4433  eldifpr  4606  elpwunsn  4632  eldiftp  4635  eldifsn  4735  difprsnss  4747  iundif2  5022  iindif1  5023  iindif2  5025  disjss3  5092  brdif  5146  dffr6  5579  difopab  5773  difopabOLD  5774  intirr  6059  cnvdif  6083  difxp  6103  xpdifid  6107  frpoind  6282  wfiOLD  6291  ordunidif  6351  onmindif  6394  imadif  6569  dffv2  6920  eldifpw  7681  releldmdifi  7955  funeldmdif  7958  ressuppssdif  8072  extmptsuppeq  8075  suppss  8081  suppssOLD  8082  suppssr  8083  suppssrg  8084  suppss2  8087  suppofssd  8090  suppcoss  8094  ondif2  8404  oelim2  8498  eldifsucnn  8566  boxcutc  8801  brsdom  8837  brsdom2  8963  php3  9078  php3OLD  9090  unblem1  9161  unfilem1  9176  elfi2  9272  dfsup2  9302  ordtypelem7  9382  ssttrcl  9573  ttrcltr  9574  dmttrcl  9579  frind  9608  kmlem4  10011  ackbij1lem18  10095  infpssr  10166  isf34lem4  10235  fin17  10252  fin67  10253  dffin7-2  10256  fin1a2lem6  10263  axcclem  10315  pwfseqlem3  10518  grothprim  10692  xrlenlt  11142  nzadd  12470  irradd  12815  irrmul  12816  difreicc  13318  modirr  13764  hashinf  14151  sumss  15536  fsumss  15537  prodss  15757  fprodss  15758  fprodn0f  15801  rpnnen2lem12  16034  dvdsaddre2b  16116  sumeven  16196  bitscmp  16245  lcmfunsnlem2  16443  iserodd  16634  prmodvdslcmf  16846  symgfix2  19121  pmtrdifellem4  19184  sylow2alem2  19320  efgsfo  19441  gsumval3  19604  gsum2dlem1  19667  gsum2dlem2  19668  ablfac1eu  19772  gsumdixp  19944  isnirred  20038  isirred2  20039  irredn0  20041  lsppratlem1  20516  lbsextlem2  20528  xrsmgmdifsgrp  20742  psgnodpm  20900  mplsubrglem  21317  mplcoe1  21345  mplcoe5  21348  opsrtoslem2  21370  symgmatr01lem  21909  elcls  22331  isclo  22345  maxlp  22405  restntr  22440  isreg2  22635  cmpcld  22660  hausdiag  22903  txkgen  22910  kqcldsat  22991  ufinffr  23187  fin1aufil  23190  alexsublem  23302  alexsubALTlem3  23307  ptcmplem5  23314  blcld  23768  shftmbl  24809  vitalilem4  24882  vitalilem5  24883  vitali  24884  mbfeqalem1  24912  itg1val2  24955  itg10a  24982  itg1ge0a  24983  mbfi1fseqlem4  24990  itg2uba  25015  itg2splitlem  25020  itg2monolem1  25022  itg2cnlem1  25033  itg2cnlem2  25034  itgss  25083  dvtaylp  25636  pserdvlem2  25694  ellogdm  25901  relogbcxp  26042  cxplogb  26043  logbmpt  26045  atandm  26133  atans2  26188  eldmgm  26278  igamgam  26305  igamf  26307  igamcl  26308  lgam1  26320  gam1  26321  wilthlem2  26325  basellem3  26339  fsumvma  26468  dchrelbas2  26492  dchreq  26513  dchrsum  26524  gausslemma2dlem4  26624  2sqreultblem  26703  dchrisum0fno1  26766  rplogsum  26782  islnopp  27390  frgrncvvdeq  28962  fusgr2wsp2nb  28987  eleigvec  30608  strlem1  30901  strlem5  30906  hstrlem5  30914  difrab2  31134  nfpconfp  31254  suppiniseg  31307  suppss3  31346  fsuppcurry1  31347  fsuppcurry2  31348  xrdifh  31388  nndiffz1  31394  ist0cld  32081  ordtconnlem1  32172  esumpinfval  32339  eulerpartlems  32627  eulerpartlemgc  32629  eulerpartlemb  32635  eulerpartlemf  32637  eulerpartlemt  32638  eulerpartlemgh  32645  ballotlemodife  32764  ballotth  32804  reprdifc  32907  hgt750lemb  32936  elmrsubrn  33781  mrsubvrs  33783  dftr6  34009  dffr5  34012  xpord2pred  34076  xpord2ind  34078  xpord3pred  34082  newbday  34192  sltlpss  34197  brsset  34330  dfon3  34333  ellimits  34351  dffun10  34355  elfuns  34356  fullfunfv  34388  dfrecs2  34391  dfrdg4  34392  dfint3  34393  hfext  34624  onsucsuccmpi  34771  bj-rest10b  35416  difunieq  35701  pibt2  35744  iundif1  35907  lindsadd  35926  poimirlem2  35935  poimirlem11  35944  poimirlem12  35945  poimirlem18  35951  poimirlem21  35954  poimirlem22  35955  poimirlem30  35963  itg2addnclem  35984  ftc1anclem5  36010  areacirc  36026  fdc  36059  isfldidl  36382  opelvvdif  36575  iswatN  38313  dochsnkrlem1  39788  selvval2lem5  40534  fsuppssindlem1  40591  ellz1  40902  pellexlem4  40967  pellexlem5  40968  infordmin  41513  minregex  41515  pwinfig  41542  elnonrel  41566  sqrtcvallem1  41612  clsk3nimkb  42023  ntrclselnel1  42040  ntrneiel2  42069  ntrneik4w  42083  undif3VD  42875  limcrecl  43558  icccncfext  43816  dvmptfprodlem  43873  stoweidlem26  43955  stoweidlem39  43968  stoweidlem52  43981  fourierdlem42  44078  etransclem18  44181  etransclem46  44209  ovolval4lem1  44576  requad01  45491  0ringdif  45846  0ring1eq0  45848  lindslinindsimp1  46216  dignn0fr  46365