Theorem eldif 3423

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 3067	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 3067	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 463	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2474	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2474	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 292	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 709	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3416	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3197	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 351	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   <-> wb 184   /\ wa 367   = wceq 1405   e. wcel 1842   _Vcvv 3058   \ cdif 3410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-dif 3416

This theorem is referenced by:  eldifd  3424  eldifad  3425  eldifbd  3426  difeqri  3562  eldifi  3564  eldifn  3565  neldif  3567  difdif  3568  ddif  3574  ssconb  3575  sscon  3576  ssdif  3577  raldifb  3582  elsymdif  3674  symdif2  3677  dfss4  3683  dfun2  3684  dfin2  3685  difin  3686  indifdir  3705  undif3  3710  difin2  3711  dfnul2  3739  reldisj  3812  disj3  3813  undif4  3825  ssdif0  3827  pssnel  3836  difin0ss  3837  inssdif0  3838  inundif  3849  ssundif  3854  eldifpr  3988  elpwunsn  4012  eldiftp  4014  eldifsn  4096  difprsnss  4106  iundif2  4337  iindif2  4339  disjss3  4393  brdif  4444  difopab  4954  intirr  5205  cnvdif  5229  difxp  5248  xpdifid  5252  wfi  5399  ordunidif  5457  onmindif  5498  imadif  5643  dffv2  5921  suppssOLD  5997  suppssrOLD  5998  suppss2OLD  6510  eldifpw  6593  ressuppssdif  6923  extmptsuppeq  6926  suppss  6932  suppssr  6933  suppss2  6936  ondif2  7188  oelim2  7280  boxcutc  7549  brsdom  7575  brsdom2  7678  php3  7740  unblem1  7805  unfilem1  7817  elfi2  7907  dfsup2  7935  dfsup2OLD  7936  ordtypelem7  7982  kmlem4  8564  ackbij1lem18  8648  infpssr  8719  isf34lem4  8788  fin17  8805  fin67  8806  dffin7-2  8809  fin1a2lem6  8816  axcclem  8868  pwfseqlem3  9067  grothprim  9241  xrlenlt  9681  irradd  11250  irrmul  11251  difreicc  11704  modirr  12096  hashinf  12455  sumss  13693  fsumss  13694  prodss  13904  fprodss  13905  rpnnen2  14166  bitscmp  14295  iserodd  14566  symgfix2  16763  pmtrdifellem4  16826  sylow2alem2  16960  efgsfo  17079  gsumval3OLD  17230  gsumval3  17233  gsum2dlem1  17316  gsum2dlem2  17317  gsum2dOLD  17319  ablfac1eu  17442  gsumdixpOLD  17575  gsumdixp  17576  isnirred  17667  isirred2  17668  irredn0  17670  lsppratlem1  18111  lbsextlem2  18123  mplsubrglem  18418  mplsubrglemOLD  18419  mplcoe1  18445  mplcoe5  18449  mplcoe2OLD  18451  opsrtoslem2  18467  xrsmgmdifsgrp  18773  psgnodpm  18920  symgmatr01lem  19445  elcls  19865  isclo  19879  maxlp  19939  restntr  19974  isreg2  20169  cmpcld  20193  hausdiag  20436  txkgen  20443  kqcldsat  20524  ufinffr  20720  fin1aufil  20723  alexsublem  20834  alexsubALTlem3  20839  ptcmplem5  20846  blcld  21298  shftmbl  22239  vitalilem4  22310  vitalilem5  22311  vitali  22312  mbfeqalem  22339  itg1val2  22381  itg10a  22407  itg1ge0a  22408  mbfi1fseqlem4  22415  itg2uba  22440  itg2splitlem  22445  itg2monolem1  22447  itg2cnlem1  22458  itg2cnlem2  22459  itgss  22508  dvtaylp  23055  pserdvlem2  23113  ellogdm  23312  relogbcxp  23450  cxplogb  23451  logbmpt  23453  atandm  23530  atans2  23585  eldmgm  23675  igamgam  23702  igamf  23704  igamcl  23705  lgam1  23717  gam1  23718  wilthlem2  23722  basellem3  23735  fsumvma  23867  dchrelbas2  23891  dchreq  23912  dchrsum  23923  dchrisum0fno1  24075  rplogsum  24091  islnopp  24496  isusgra0  24751  usgraop  24754  nbcusgra  24867  frgraunss  25399  frgrancvvdeqlem3  25436  frgrancvvdeqlem9  25445  frgrawopreglem3  25450  frgrawopreglem4  25451  frgrawopreg  25453  usg2spot2nb  25469  eleigvec  27275  strlem1  27568  strlem5  27573  hstrlem5  27581  suppss2f  27906  suppss3  27983  xrdifh  28025  nndiffz1  28030  ordtconlem1  28345  esumpinfval  28506  eulerpartlems  28791  eulerpartlemgc  28793  eulerpartlemb  28799  eulerpartlemf  28801  eulerpartlemt  28802  eulerpartlemgh  28809  ballotlemodife  28928  ballotth  28968  elmrsubrn  29719  mrsubvrs  29721  dftr6  29950  dffr5  29953  frind  30041  brsset  30214  dfon3  30217  ellimits  30235  dffun10  30239  elfuns  30240  fullfunfv  30272  dfrecs2  30275  dfrdg4  30276  dfint3  30277  hfext  30508  onsucsuccmpi  30662  iundif1  31389  dvtanlemOLD  31417  itg2addnclem  31419  ftc1anclem5  31447  areacirc  31463  fdc  31500  isfldidl  31727  iswatN  32991  dochsnkrlem1  34469  ellz1  35041  pellexlem4  35109  pellexlem5  35110  pwinfig  35592  compel  36175  undif3VD  36693  fprodn0f  36943  limcrecl  36984  icccncfext  37039  dvmptfprodlem  37090  stoweidlem26  37157  stoweidlem39  37170  stoweidlem52  37183  fourierdlem42  37280  etransclem18  37384  etransclem46  37412  uhgraedgrnv  37959  0ringdif  38168  0ring1eq0  38170  lindslinindsimp1  38550  dignn0fr  38713