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

Theorem difexg 5285
Description: Existence of a difference. (Contributed by NM, 26-May-1998.)
Assertion
Ref Expression
difexg (𝐴𝑉 → (𝐴𝐵) ∈ V)

Proof of Theorem difexg
StepHypRef Expression
1 difss 4092 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 5281 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 689 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3444  cdif 3908  wss 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-in 3918  df-ss 3928
This theorem is referenced by:  difexi  5286  difexd  5287  difex2  7695  elpwun  7704  2oconcl  8450  fnoe  8457  difsnen  9000  sucdom2OLD  9029  fodomr  9075  domss2  9083  domssex2  9084  domssex  9085  limenpsi  9099  dif1enlem  9103  sucdom2  9153  brwdom2  9514  infeq5i  9577  infdifsn  9598  dfac8clem  9973  ssfin4  10251  isf34lem1  10313  compssiso  10315  fin1a2lem7  10347  fin1a2lem13  10353  fpwwe2lem12  10583  hashgt23el  14330  hashf1lem1OLD  14360  pmtrfv  19239  isirred  20135  isdrng2  20210  drngmcl  20213  drngid2  20216  isdrngd  20226  isdrngdOLD  20228  subdrgint  20284  cnmsubglem  20876  islindf4  21260  smadiadetlem1a  22028  basdif0  22319  tgdif0  22358  clsval2  22417  cmpcld  22769  ptcmplem2  23420  iunmbl  24933  tdeglem4OLD  25441  logbfval  26156  nbfusgrlevtxm2  28368  vtxdginducedm1  28533  frgrwopreglem1  29298  eigvecval  30880  elpwdifcl  31497  disjdifprg  31539  mptiffisupp  31654  padct  31683  resf1o  31694  xrge00  31926  xrge0tsmsd  31948  tocycf  32015  ist0cld  32471  locfinref  32479  ldsysgenld  32816  sigapildsys  32818  carsgclctun  32978  sitgclg  32999  ballotlemfrc  33183  ballotlem8  33193  bnj852  33590  bnj865  33592  subfacp1lem5  33835  iscvm  33910  cvmsval  33917  mdvval  34155  topdifinffinlem  35864  pibt2  35934  poimirlem15  36139  voliunnfl  36168  fdc  36250  isdrngo2  36463  lzenom  41136  diophin  41138  diophren  41179  deg1mhm  41577  stoweidlem57  44384  fourierdlem102  44535  fourierdlem114  44547  pwsal  44642  gsumge0cl  44698  caragendifcl  44841  carageniuncllem1  44848  isomenndlem  44857  hoidmv1lelem2  44919  lincdifsn  46591  lindslinindsimp1  46624  lindslinindimp2lem2  46626  lindslinindimp2lem4  46628  lindslinindsimp2lem5  46629  lindslinindsimp2  46630  lincresunit1  46644  lincresunit2  46645  lincresunit3lem2  46647  lincresunit3  46648
  Copyright terms: Public domain W3C validator