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

Theorem eldif 3332
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 2966 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2966 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 453 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2498 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2498 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 287 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 693 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3325 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 3086 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 344 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   _Vcvv 2958    \ cdif 3319
This theorem is referenced by:  eldifd  3333  eldifad  3334  eldifbd  3335  difeqri  3469  eldifi  3471  eldifn  3472  neldif  3474  difdif  3475  ddif  3481  ssconb  3482  sscon  3483  ssdif  3484  raldifb  3489  dfss4  3577  dfun2  3578  dfin2  3579  difin  3580  indifdir  3599  undif3  3604  difin2  3605  symdif2  3609  dfnul2  3632  reldisj  3673  disj3  3674  undif4  3686  ssdif0  3688  pssnel  3695  difin0ss  3696  inssdif0  3697  inundif  3708  ssundif  3713  eldifsn  3929  difprsnss  3936  iundif2  4160  iindif2  4162  disjss3  4214  brdif  4263  ordunidif  4632  onmindif  4674  eldifpw  4758  elpwunsn  4760  difopab  5009  intirr  5255  cnvdif  5281  imadif  5531  dffv2  5799  suppss  5866  suppssr  5867  suppss2  6303  difxp  6383  ondif2  6749  oelim2  6841  boxcutc  7108  brsdom  7133  brsdom2  7234  php3  7296  unblem1  7362  unfilem1  7374  elfi2  7422  dfsup2  7450  dfsup2OLD  7451  ordtypelem7  7496  cantnfreslem  7634  kmlem4  8038  ackbij1lem18  8122  infpssr  8193  isf34lem4  8262  fin17  8279  fin67  8280  dffin7-2  8283  fin1a2lem6  8290  axcclem  8342  pwfseqlem3  8540  grothprim  8714  xrlenlt  9148  irradd  10603  irrmul  10604  difreicc  11033  modirr  11291  hashinf  11628  sumss  12523  fsumss  12524  rpnnen2  12830  bitscmp  12955  iserodd  13214  sylow2alem2  15257  efgsfo  15376  gsumval3  15519  gsum2d  15551  ablfac1eu  15636  gsumdixp  15720  isnirred  15810  isirred2  15811  irredn0  15813  lsppratlem1  16224  lbsextlem2  16236  mplsubrglem  16507  mplcoe1  16533  mplcoe2  16535  opsrtoslem2  16550  elcls  17142  isclo  17156  maxlp  17216  restntr  17251  isreg2  17446  cmpcld  17470  hausdiag  17682  txkgen  17689  kqcldsat  17770  ufinffr  17966  fin1aufil  17969  alexsublem  18080  alexsubALTlem3  18085  ptcmplem5  18092  blcld  18540  shftmbl  19438  vitalilem4  19508  vitalilem5  19509  vitali  19510  mbfeqalem  19537  itg1val2  19579  itg10a  19605  itg1ge0a  19606  mbfi1fseqlem4  19613  itg2uba  19638  itg2splitlem  19643  itg2monolem1  19645  itg2cnlem1  19656  itg2cnlem2  19657  itgss  19706  dvtaylp  20291  pserdvlem2  20349  ellogdm  20535  atandm  20721  atans2  20776  wilthlem2  20857  basellem3  20870  fsumvma  21002  dchrelbas2  21026  dchreq  21047  dchrsum  21058  dchrisum0fno1  21210  rplogsum  21226  isusgra0  21381  nbcusgra  21477  eleigvec  23465  strlem1  23758  strlem5  23763  hstrlem5  23771  suppss2f  24054  xrdifh  24148  eldifpr  24397  eldiftp  24398  esumpinfval  24468  sibfof  24659  ballotlemodife  24760  ballotth  24800  eldmgm  24811  igamgam  24838  igamf  24840  igamcl  24841  lgam1  24853  gam1  24854  prodss  25278  fprodss  25279  dftr6  25378  dffr5  25381  wfi  25487  frind  25523  elsymdif  25673  brsset  25739  dfon3  25742  ellimits  25760  dffun10  25764  elfuns  25765  fullfunfv  25797  dfrdg4  25800  tfrqfree  25801  dfint3  25802  hfext  26129  onsucsuccmpi  26198  iundif1  26244  dvtanlem  26268  itg2addnclem  26270  ftc1anclem5  26298  areacirc  26311  fdc  26463  isfldidl  26692  ellz1  26839  pellexlem4  26909  pellexlem5  26910  compel  27631  stoweidlem26  27765  stoweidlem39  27778  stoweidlem52  27791  uhgraedgrnv  28326  frgraunss  28459  frgrancvvdeqlem3  28495  frgrancvvdeqlem9  28504  frgrawopreglem3  28509  frgrawopreglem4  28510  frgrawopreg  28512  usg2spot2nb  28528  undif3VD  29068  iswatN  30865  dochsnkrlem1  32341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325
  Copyright terms: Public domain W3C validator