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

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

Proof of Theorem difexg
StepHypRef Expression
1 difss 3721 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 4774 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 705 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Vcvv 3190  cdif 3557  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563  df-in 3567  df-ss 3574
This theorem is referenced by:  difexi  4779  difexOLD  4780  difex2  6933  elpwun  6939  2oconcl  7543  fnoe  7550  ralxpmap  7867  difsnen  8002  domdifsn  8003  domunsncan  8020  fodomr  8071  domss2  8079  domssex2  8080  domssex  8081  mapdom2  8091  limenpsi  8095  sucdom2  8116  findcard  8159  findcard2  8160  frfi  8165  unfilem3  8186  brwdom2  8438  infeq5i  8493  infdifsn  8514  dfac8clem  8815  acni  8828  dfac9  8918  dfacacn  8923  infpss  8999  ssfin4  9092  fin23lem28  9122  isf32lem6  9140  isf32lem7  9141  isf32lem8  9142  isf34lem1  9154  compssiso  9156  enfin1ai  9166  fin1a2lem7  9188  fin1a2lem13  9194  axdc2lem  9230  axcclem  9239  zornn0g  9287  fpwwe2lem13  9424  fpwwe2  9425  canthp1lem1  9434  grothprim  9616  hashbclem  13190  hashf1lem1  13193  fi1uzind  13234  brfi1uzind  13235  brfi1indALT  13237  opfi1uzind  13238  fi1uzindOLD  13240  brfi1uzindOLD  13241  brfi1indALTOLD  13243  opfi1uzindOLD  13244  ramub1lem1  15673  mrieqv2d  16239  mreexexlemd  16244  pltfval  16899  pmtrfv  17812  dpjidcl  18397  isirred  18639  isdrng2  18697  drngmcl  18700  drngid2  18703  isdrngd  18712  lssset  18874  xrs1mnd  19724  xrs1cmn  19726  xrge0subm  19727  cnmsubglem  19749  islindf4  20117  smadiadetlem1a  20409  basdif0  20697  tgdif0  20736  clsval2  20794  neitr  20924  lecldbas  20963  pnrmopn  21087  cmpcld  21145  cmpfi  21151  csdfil  21638  ufileu  21663  filufint  21664  alexsublem  21788  ptcmplem2  21797  xrge0gsumle  22576  xrge0tsms  22577  bcth3  23068  iunmbl  23261  i1fd  23388  tdeglem4  23758  reefgim  24142  logbmpt  24460  logbfval  24462  axlowdimlem15  25770  axlowdim  25775  elntg  25798  nbfusgrlevtxm1  26200  nbfusgrlevtxm2  26201  cusgrfilem3  26274  frgrwopreglem1  27073  eigvecval  28643  elpwdifcl  29246  disjdifprg  29274  padct  29381  resf1o  29389  xrge00  29513  xrge0tsmsd  29612  locfinref  29732  esummono  29939  esumpad  29940  esumpad2  29941  insiga  30023  ldsysgenld  30046  sigapildsys  30048  carsgclctun  30206  sitgclg  30227  ballotlemfrc  30411  ballotlem8  30421  bnj852  30752  bnj865  30754  subfacp1lem5  30927  iscvm  31002  cvmsval  31009  mdvval  31162  topdifinffinlem  32866  poimirlem15  33095  voliunnfl  33124  fdc  33212  isdrngo2  33428  watvalN  34798  hvmapfval  36567  lzenom  36852  diophin  36855  diophren  36896  cntzsdrg  37292  deg1mhm  37305  sssymdifcl  37397  clcnvlem  37450  dssmapfv3d  37834  dssmapnvod  37835  ovolsplit  39542  stoweidlem57  39611  fourierdlem102  39762  fourierdlem114  39774  pwsal  39872  intsal  39885  gsumge0cl  39925  sge0ss  39966  sge0fodjrnlem  39970  iundjiunlem  40013  iundjiun  40014  meaiunlelem  40022  caragendifcl  40065  carageniuncllem1  40072  isomenndlem  40081  hoidmv1lelem2  40143  lincdifsn  41531  lindslinindsimp1  41564  lindslinindimp2lem2  41566  lindslinindimp2lem4  41568  lindslinindsimp2lem5  41569  lindslinindsimp2  41570  lincresunit1  41584  lincresunit2  41585  lincresunit3lem2  41587  lincresunit3  41588
  Copyright terms: Public domain W3C validator