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

Theorem difexi 5218
Description: Existence of a difference, inference version of difexg 5217. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.)
Hypothesis
Ref Expression
difexi.1 𝐴 ∈ V
Assertion
Ref Expression
difexi (𝐴𝐵) ∈ V

Proof of Theorem difexi
StepHypRef Expression
1 difexi.1 . 2 𝐴 ∈ V
2 difexg 5217 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  Vcvv 3480  cdif 3916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-sep 5189
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-v 3482  df-dif 3922  df-in 3926  df-ss 3936
This theorem is referenced by:  oev  8135  sbthlem2  8625  phplem2  8694  php  8698  pssnn  8733  findcard  8754  findcard2  8755  frfi  8760  unfilem3  8781  marypha1lem  8894  inf3lem3  9090  dfac9  9560  dfacacn  9565  kmlem11  9584  kmlem12  9585  fin23lem28  9760  isf32lem6  9778  isf32lem7  9779  isf32lem8  9780  domtriomlem  9862  axdc2lem  9868  axcclem  9877  zornn0g  9925  konigthlem  9988  grothprim  10254  hashbclem  13815  fi1uzind  13860  brfi1uzind  13861  brfi1indALT  13863  opfi1uzind  13864  ramub1lem1  16360  pltfval  17569  isirred  19452  cntzsdrg  19581  subdrgint  19582  lssset  19705  xrs1mnd  20583  xrs10  20584  xrs1cmn  20585  xrge0subm  20586  xrge0cmn  20587  cnmsgngrp  20723  psgninv  20726  neitr  21788  lecldbas  21827  imasdsf1olem  22983  xrge0gsumle  23441  xrge0tsms  23442  i1fd  24288  lhop1lem  24619  reefgim  25048  cxpcn2  25338  logbmpt  25377  axlowdimlem15  26753  axlowdim  26758  elntg  26781  uhgrspan1lem1  27093  upgrres1lem1  27102  nbgrval  27129  nbfusgrlevtxm1  27170  cusgrfilem3  27250  vtxdginducedm1lem1  27332  vtxdginducedm1fi  27337  finsumvtxdg2ssteplem4  27341  dimkerim  31083  satfv1lem  32666  satfdm  32673  satffunlem1lem2  32707  satffunlem2lem2  32710  watvalN  37234  hvmapfval  39000  prjspval  39513  setindtr  39881  ssdifcl  40186  sssymdifcl  40187  clsk3nimkb  40662  iundjiunlem  43024  meaiuninclem  43045  meaiininclem  43051  lines  45071
  Copyright terms: Public domain W3C validator