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

Theorem difexg 4564
Description: Existence of a difference. (Contributed by NM, 26-May-1998.)
Assertion
Ref Expression
difexg  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )

Proof of Theorem difexg
StepHypRef Expression
1 difss 3571 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4562 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 681 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1897   _Vcvv 3056    \ cdif 3412    C_ wss 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-dif 3418  df-in 3422  df-ss 3429
This theorem is referenced by:  difex2  6624  elpwun  6630  2oconcl  7230  fnoe  7237  ralxpmap  7546  difsnen  7679  domdifsn  7680  domunsncan  7697  fodomr  7748  domss2  7756  domssex2  7757  domssex  7758  mapdom2  7768  limenpsi  7772  sucdom2  7793  findcard  7835  findcard2  7836  frfi  7841  unfilem3  7862  marypha1lem  7972  brwdom2  8113  infeq5i  8166  infdifsn  8187  dfac8clem  8488  acni  8501  dfac9  8591  dfacacn  8596  kmlem11  8615  kmlem12  8616  infpss  8672  ssfin4  8765  fin23lem28  8795  isf32lem6  8813  isf32lem7  8814  isf32lem8  8815  isf34lem1  8827  compssiso  8829  enfin1ai  8839  fin1a2lem7  8861  fin1a2lem13  8867  axdc2lem  8903  axcclem  8912  zornn0g  8960  fpwwe2lem13  9092  fpwwe2  9093  canthp1lem1  9102  grothprim  9284  hashbclem  12647  hashf1lem1  12650  fi1uzind  12682  brfi1uzind  12683  brfi1indALT  12685  opfi1uzind  12686  ramub1lem1  15032  mrieqv2d  15593  mreexexlemd  15598  pltfval  16253  pmtrfv  17141  dpjidcl  17739  isirred  17975  isdrng2  18033  drngmcl  18036  drngid2  18039  isdrngd  18048  lssset  18205  xrs1mnd  19054  xrs1cmn  19056  xrge0subm  19057  cnmsubglem  19078  islindf4  19444  smadiadetlem1a  19736  basdif0  20016  tgdif0  20056  clsval2  20113  neitr  20244  lecldbas  20283  pnrmopn  20407  cmpcld  20465  cmpfi  20471  csdfil  20957  ufileu  20982  filufint  20983  alexsublem  21107  ptcmplem2  21116  xrge0gsumle  21899  xrge0tsms  21900  bcth3  22347  iunmbl  22554  i1fd  22687  tdeglem4  23057  reefgim  23453  logbmpt  23773  logbfval  23775  axlowdimlem15  25034  axlowdim  25039  elntg  25062  usgrares1  25186  cusgrares  25248  cusgrafilem3  25257  nbhashuvtx1  25691  frgrawopreglem1  25820  ablomul  26131  eigvecval  27597  elpwdifcl  28203  disjdifprg  28233  padct  28355  resf1o  28363  xrge00  28496  xrge0tsmsd  28596  locfinref  28716  esummono  28923  esumpad  28924  esumpad2  28925  insiga  29007  ldsysgenld  29030  sigapildsys  29032  carsgclctun  29201  sitgclg  29223  ballotlemfrc  29407  ballotlem8  29417  ballotlemfrcOLD  29445  ballotlem8OLD  29455  bnj852  29780  bnj865  29782  subfacp1lem5  29955  iscvm  30030  cvmsval  30037  mdvval  30190  topdifinffinlem  31794  poimirlem15  31999  voliunnfl  32028  fdc  32118  isdrngo2  32241  watvalN  33602  hvmapfval  35371  lzenom  35656  diophin  35659  diophren  35700  cntzsdrg  36112  deg1mhm  36128  ssdifcl  36219  sssymdifcl  36220  clcnvlem  36274  stoweidlem57  37955  fourierdlem102  38109  fourierdlem114  38121  pwsal  38213  intsal  38226  gsumge0cl  38250  sge0ss  38291  sge0fodjrnlem  38295  iundjiunlem  38334  iundjiun  38335  meaiunlelem  38343  caragendifcl  38372  carageniuncllem1  38379  isomenndlem  38388  hoidmv1lelem2  38451  uhgrspan1lem1  39421  upgrres1lem1  39425  nbgrval  39455  nbfusgrlevtxm1  39500  nbfusgrlevtxm2  39501  cusgrfilem3  39567  usgresvm1  40027  usgresvm1ALT  40031  lincdifsn  40489  lindslinindsimp1  40522  lindslinindimp2lem2  40524  lindslinindimp2lem4  40526  lindslinindsimp2lem5  40527  lindslinindsimp2  40528  lincresunit1  40542  lincresunit2  40543  lincresunit3lem2  40545  lincresunit3  40546
  Copyright terms: Public domain W3C validator