Theorem eldif 3443

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 3087	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 3087	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 466	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2492	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2492	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 295	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 715	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3436	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3217	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 354	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1867   _Vcvv 3078   \ cdif 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-dif 3436

This theorem is referenced by:  eldifd  3444  eldifad  3445  eldifbd  3446  difeqri  3582  eldifi  3584  eldifn  3585  neldif  3587  difdif  3588  ddif  3594  ssconb  3595  sscon  3596  ssdif  3597  raldifb  3602  elsymdif  3695  symdif2  3698  dfss4  3704  dfun2  3705  dfin2  3706  difin  3707  indifdir  3726  undif3  3731  difin2  3732  dfnul2  3760  reldisj  3833  disj3  3834  undif4  3846  ssdif0  3848  pssnel  3857  difin0ss  3858  inssdif0  3859  inundif  3870  ssundif  3876  eldifpr  4010  elpwunsn  4034  eldiftp  4037  eldifsn  4119  difprsnss  4129  iundif2  4360  iindif2  4362  disjss3  4416  brdif  4468  difopab  4978  intirr  5230  cnvdif  5254  difxp  5273  xpdifid  5277  wfi  5424  ordunidif  5482  onmindif  5523  imadif  5668  dffv2  5946  eldifpw  6609  ressuppssdif  6939  extmptsuppeq  6942  suppss  6948  suppssr  6949  suppss2  6952  ondif2  7204  oelim2  7296  boxcutc  7565  brsdom  7591  brsdom2  7694  php3  7756  unblem1  7821  unfilem1  7833  elfi2  7926  dfsup2  7956  ordtypelem7  8037  kmlem4  8579  ackbij1lem18  8663  infpssr  8734  isf34lem4  8803  fin17  8820  fin67  8821  dffin7-2  8824  fin1a2lem6  8831  axcclem  8883  pwfseqlem3  9081  grothprim  9255  xrlenlt  9695  irradd  11284  irrmul  11285  difreicc  11758  modirr  12153  hashinf  12513  sumss  13768  fsumss  13769  prodss  13979  fprodss  13980  fprodn0f  14023  rpnnen2  14256  bitscmp  14390  lcmfunsnlem2  14591  iserodd  14763  prmodvdslcmf  14983  prmordvdslcmfOLD  14997  prmordvdslcmsOLDOLD  14999  symgfix2  17035  pmtrdifellem4  17098  sylow2alem2  17248  efgsfo  17367  gsumval3  17519  gsum2dlem1  17580  gsum2dlem2  17581  ablfac1eu  17684  gsumdixp  17815  isnirred  17906  isirred2  17907  irredn0  17909  lsppratlem1  18348  lbsextlem2  18360  mplsubrglem  18641  mplcoe1  18667  mplcoe5  18670  opsrtoslem2  18686  xrsmgmdifsgrp  18983  psgnodpm  19133  symgmatr01lem  19655  elcls  20066  isclo  20080  maxlp  20140  restntr  20175  isreg2  20370  cmpcld  20394  hausdiag  20637  txkgen  20644  kqcldsat  20725  ufinffr  20921  fin1aufil  20924  alexsublem  21036  alexsubALTlem3  21041  ptcmplem5  21048  blcld  21497  shftmbl  22469  vitalilem4  22546  vitalilem5  22547  vitali  22548  mbfeqalem  22575  itg1val2  22619  itg10a  22645  itg1ge0a  22646  mbfi1fseqlem4  22653  itg2uba  22678  itg2splitlem  22683  itg2monolem1  22685  itg2cnlem1  22696  itg2cnlem2  22697  itgss  22746  dvtaylp  23302  pserdvlem2  23360  ellogdm  23561  relogbcxp  23699  cxplogb  23700  logbmpt  23702  atandm  23779  atans2  23834  eldmgm  23924  igamgam  23951  igamf  23953  igamcl  23954  lgam1  23966  gam1  23967  wilthlem2  23971  basellem3  23986  fsumvma  24118  dchrelbas2  24142  dchreq  24163  dchrsum  24174  dchrisum0fno1  24326  rplogsum  24342  islnopp  24758  isusgra0  25051  usgraop  25054  nbcusgra  25167  frgraunss  25699  frgrancvvdeqlem3  25736  frgrancvvdeqlem9  25745  frgrawopreglem3  25750  frgrawopreglem4  25751  frgrawopreg  25753  usg2spot2nb  25769  eleigvec  27586  strlem1  27879  strlem5  27884  hstrlem5  27892  suppss2fOLD  28218  suppss3  28297  xrdifh  28347  nndiffz1  28351  ordtconlem1  28719  esumpinfval  28883  eulerpartlems  29182  eulerpartlemgc  29184  eulerpartlemb  29190  eulerpartlemf  29192  eulerpartlemt  29193  eulerpartlemgh  29200  ballotlemodife  29319  ballotth  29359  ballotthOLD  29397  elmrsubrn  30147  mrsubvrs  30149  dftr6  30378  dffr5  30381  frind  30469  brsset  30642  dfon3  30645  ellimits  30663  dffun10  30667  elfuns  30668  fullfunfv  30700  dfrecs2  30703  dfrdg4  30704  dfint3  30705  hfext  30936  onsucsuccmpi  31089  iundif1  31835  poimirlem2  31850  poimirlem11  31859  poimirlem12  31860  poimirlem18  31866  poimirlem21  31869  poimirlem22  31870  poimirlem30  31878  dvtanlemOLD  31899  itg2addnclem  31901  ftc1anclem5  31929  areacirc  31945  fdc  31982  isfldidl  32209  iswatN  33472  dochsnkrlem1  34950  ellz1  35522  pellexlem4  35590  pellexlem5  35591  pwinfig  36079  compel  36643  undif3VD  37134  limcrecl  37496  icccncfext  37552  dvmptfprodlem  37606  stoweidlem26  37673  stoweidlem39  37687  stoweidlem52  37700  fourierdlem42  37799  fourierdlem42OLD  37800  etransclem18  37904  etransclem46  37932  uhgraedgrnv  38725  0ringdif  38932  0ring1eq0  38934  lindslinindsimp1  39314  dignn0fr  39477