MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldif Unicode version

Theorem eldif 3162
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.
StepHypRef Expression
1 elex 2796 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2796 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 451 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2343 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2343 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 285 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 691 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3155 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 2916 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 342 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   _Vcvv 2788    \ cdif 3149
This theorem is referenced by:  eldifd  3163  eldifad  3164  eldifbd  3165  difeqri  3296  eldifi  3298  eldifn  3299  neldif  3301  difdif  3302  ddif  3308  ssconb  3309  sscon  3310  ssdif  3311  dfss4  3403  dfun2  3404  dfin2  3405  difin  3406  indifdir  3425  undif3  3429  difin2  3430  symdif2  3434  dfnul2  3457  reldisj  3498  disj3  3499  undif4  3511  ssdif0  3513  pssnel  3519  difin0ss  3520  inssdif0  3521  inundif  3532  ssundif  3537  eldifsn  3749  difprsn  3756  iundif2  3969  iindif2  3971  disjss3  4022  brdif  4071  pwundifOLD  4301  ordunidif  4440  onmindif  4482  eldifpw  4566  elpwunsn  4568  difopab  4817  intirr  5061  cnvdif  5087  imadif  5327  dffv2  5592  suppss  5658  suppssr  5659  suppss2  6073  difxp  6153  ondif2  6501  oaf1o  6561  oelim2  6593  boxcutc  6859  brsdom  6884  brsdom2  6985  php3  7047  unblem1  7109  unfilem1  7121  elfi2  7168  dfsup2  7195  dfsup2OLD  7196  ordtypelem7  7239  infeq5i  7337  cantnfreslem  7377  cantnflem1  7391  cantnflem2  7392  kmlem4  7779  ackbij1lem18  7863  infpssr  7934  fin23lem26  7951  isf34lem4  8003  fin17  8020  fin67  8021  isfin7-2  8022  dffin7-2  8024  fin1a2lem6  8031  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  ttukeylem7  8142  pwfseqlem1  8280  pwfseqlem3  8282  grothprim  8456  xrlenlt  8890  irradd  10340  irrmul  10341  difreicc  10767  modirr  11009  hashinf  11342  hashf1lem1  11393  seqcoll  11401  seqcoll2  11402  rlimcld2  12052  sumrblem  12184  fsumcvg  12185  sumss  12197  fsumss  12198  rpnnen2  12504  ruclem12  12519  bitscmp  12629  iserodd  12888  prmreclem5  12967  ramub1lem1  13073  sylow2alem2  14929  efgsfo  15048  frgpnabllem1  15161  gsumval3  15191  gsumzaddlem  15203  gsum2d  15223  dmdprdsplitlem  15272  ablfac1eu  15308  pgpfac1lem2  15310  pgpfac1lem3  15312  gsumdixp  15392  isnirred  15482  isirred2  15483  irredn0  15485  irredrmul  15489  lsppratlem1  15900  lsppratlem3  15902  lbsextlem2  15912  lbsextlem4  15914  mplsubrglem  16183  mplcoe1  16209  mplcoe2  16211  opsrtoslem2  16226  elcls  16810  isclo  16824  maxlp  16878  restntr  16912  regsep2  17104  isreg2  17105  cmpcld  17129  1stckgen  17249  hausdiag  17339  txkgen  17346  kqcldsat  17424  regr1lem  17430  ufinffr  17624  fin1aufil  17627  alexsublem  17738  alexsubALTlem3  17743  ptcmplem5  17750  opnsubg  17790  blcld  18051  zcld  18319  recld2  18320  bcthlem4  18749  shftmbl  18896  iundisj  18905  vitalilem4  18966  vitalilem5  18967  vitali  18968  mbfeqalem  18997  itg1val2  19039  itg10a  19065  itg1ge0a  19066  mbfi1fseqlem4  19073  itg2uba  19098  itg2splitlem  19103  itg2monolem1  19105  itg2cnlem1  19116  itg2cnlem2  19117  iblss2  19160  itgss  19166  itgeqa  19168  limcnlp  19228  dvtaylp  19749  pserdvlem2  19804  ellogdm  19986  dvloglem  19995  dvlog2lem  19999  atandm  20172  atans2  20227  ressatans  20230  wilthlem2  20307  ftalem3  20312  basellem3  20320  fsumvma  20452  dchrelbas2  20476  dchreq  20497  dchrsum  20508  dchrisum0fno1  20660  rplogsum  20676  eleigvec  22537  strlem1  22830  strlem5  22835  hstrlem5  22843  ballotlemodife  23056  suppss2f  23201  xrdifh  23273  iundisjfi  23363  iundisjf  23365  eldifpr  23394  eldiftp  23395  esumpinfval  23441  eldmgm  23694  dftr6  24107  dffr5  24110  wfi  24207  frind  24243  elsymdif  24367  brsset  24429  dfon3  24432  ellimits  24450  elfuns  24454  fullfunfv  24485  dfrdg4  24488  tfrqfree  24489  hfext  24813  onsucsuccmpi  24882  onint1  24888  areacirc  24931  difeqri2  25040  deref  25288  gltpntl2  26073  lppotos  26144  pdiveql  26168  abhp  26173  fdc  26455  isfldidl  26693  pridlc3  26698  prtlem80  26724  ellz1  26846  pellexlem4  26917  pellexlem5  26918  rmspecsqrnq  26991  rmspecnonsq  26992  frlmsslsp  27248  compel  27640  stoweidlem26  27775  stoweidlem34  27783  stoweidlem39  27788  stoweidlem52  27801  stoweidlem57  27806  stirlinglem8  27830  isusgra0  28106  nbcusgra  28159  undif3VD  28658  iswatN  30183  dochsnkrlem1  31659
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155
  Copyright terms: Public domain W3C validator