Theorem eldif 3400

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
eldif	|- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Proof of Theorem eldif

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3040	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 3040	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 472	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2537	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2537	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 301	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 725	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3393	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3175	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 360	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   <-> wb 189   /\ wa 376   = wceq 1452   e. wcel 1904   _Vcvv 3031   \ cdif 3387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393

This theorem is referenced by:  eldifd  3401  eldifad  3402  eldifbd  3403  difeqri  3542  eldifi  3544  eldifn  3545  neldif  3547  difdif  3548  ddif  3554  ssconb  3555  sscon  3556  ssdif  3557  raldifb  3562  elsymdif  3659  symdif2  3662  dfss4  3668  dfun2  3669  dfin2  3670  difin  3671  indifdir  3690  undif3  3695  difin2  3696  dfnul2  3724  ssdif0  3741  difin0ss  3745  inssdif0  3746  reldisj  3812  disj3  3813  undif4  3825  pssnel  3829  inundif  3836  ssundif  3842  eldifpr  3982  elpwunsn  4003  eldiftp  4006  eldifsn  4088  difprsnss  4098  iundif2  4336  iindif2  4338  disjss3  4394  brdif  4446  difopab  4971  intirr  5224  cnvdif  5248  difxp  5267  xpdifid  5271  wfi  5420  ordunidif  5478  onmindif  5519  imadif  5668  dffv2  5953  eldifpw  6622  ressuppssdif  6955  extmptsuppeq  6958  suppss  6964  suppssr  6965  suppss2  6968  ondif2  7222  oelim2  7314  boxcutc  7583  brsdom  7610  brsdom2  7714  php3  7776  unblem1  7841  unfilem1  7853  elfi2  7946  dfsup2  7976  ordtypelem7  8057  kmlem4  8601  ackbij1lem18  8685  infpssr  8756  isf34lem4  8825  fin17  8842  fin67  8843  dffin7-2  8846  fin1a2lem6  8853  axcclem  8905  pwfseqlem3  9103  grothprim  9277  xrlenlt  9717  irradd  11311  irrmul  11312  difreicc  11790  modirr  12194  hashinf  12558  sumss  13867  fsumss  13868  prodss  14078  fprodss  14079  fprodn0f  14122  rpnnen2  14355  bitscmp  14491  lcmfunsnlem2  14692  iserodd  14864  prmodvdslcmf  15084  prmordvdslcmfOLD  15098  prmordvdslcmsOLDOLD  15100  symgfix2  17135  pmtrdifellem4  17198  sylow2alem2  17348  efgsfo  17467  gsumval3  17619  gsum2dlem1  17680  gsum2dlem2  17681  ablfac1eu  17784  gsumdixp  17915  isnirred  18006  isirred2  18007  irredn0  18009  lsppratlem1  18448  lbsextlem2  18460  mplsubrglem  18740  mplcoe1  18766  mplcoe5  18769  opsrtoslem2  18785  xrsmgmdifsgrp  19082  psgnodpm  19233  symgmatr01lem  19755  elcls  20166  isclo  20180  maxlp  20240  restntr  20275  isreg2  20470  cmpcld  20494  hausdiag  20737  txkgen  20744  kqcldsat  20825  ufinffr  21022  fin1aufil  21025  alexsublem  21137  alexsubALTlem3  21142  ptcmplem5  21149  blcld  21598  shftmbl  22570  vitalilem4  22648  vitalilem5  22649  vitali  22650  mbfeqalem  22677  itg1val2  22721  itg10a  22747  itg1ge0a  22748  mbfi1fseqlem4  22755  itg2uba  22780  itg2splitlem  22785  itg2monolem1  22787  itg2cnlem1  22798  itg2cnlem2  22799  itgss  22848  dvtaylp  23404  pserdvlem2  23462  ellogdm  23663  relogbcxp  23801  cxplogb  23802  logbmpt  23804  atandm  23881  atans2  23936  eldmgm  24026  igamgam  24053  igamf  24055  igamcl  24056  lgam1  24068  gam1  24069  wilthlem2  24073  basellem3  24088  fsumvma  24220  dchrelbas2  24244  dchreq  24265  dchrsum  24276  dchrisum0fno1  24428  rplogsum  24444  islnopp  24860  isusgra0  25153  usgraop  25156  nbcusgra  25270  frgraunss  25802  frgrancvvdeqlem3  25839  frgrancvvdeqlem9  25848  frgrawopreglem3  25853  frgrawopreglem4  25854  frgrawopreg  25856  usg2spot2nb  25872  eleigvec  27691  strlem1  27984  strlem5  27989  hstrlem5  27997  suppss2fOLD  28313  suppss3  28387  xrdifh  28437  nndiffz1  28441  ordtconlem1  28804  esumpinfval  28968  eulerpartlems  29266  eulerpartlemgc  29268  eulerpartlemb  29274  eulerpartlemf  29276  eulerpartlemt  29277  eulerpartlemgh  29284  ballotlemodife  29403  ballotth  29443  ballotthOLD  29481  elmrsubrn  30230  mrsubvrs  30232  dftr6  30461  dffr5  30464  frind  30552  brsset  30727  dfon3  30730  ellimits  30748  dffun10  30752  elfuns  30753  fullfunfv  30785  dfrecs2  30788  dfrdg4  30789  dfint3  30790  hfext  31021  onsucsuccmpi  31174  iundif1  31991  poimirlem2  32006  poimirlem11  32015  poimirlem12  32016  poimirlem18  32022  poimirlem21  32025  poimirlem22  32026  poimirlem30  32034  dvtanlemOLD  32055  itg2addnclem  32057  ftc1anclem5  32085  areacirc  32101  fdc  32138  isfldidl  32365  iswatN  33630  dochsnkrlem1  35108  ellz1  35680  pellexlem4  35747  pellexlem5  35748  pwinfig  36236  elnonrel  36262  compel  36861  undif3VD  37342  limcrecl  37806  icccncfext  37862  dvmptfprodlem  37916  stoweidlem26  37998  stoweidlem39  38012  stoweidlem52  38025  fourierdlem42  38124  fourierdlem42OLD  38125  etransclem18  38229  etransclem46  38257  ovolval4lem1  38589  uhgraedgrnv  40172  0ringdif  40378  0ring1eq0  40380  lindslinindsimp1  40758  dignn0fr  40920