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

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

Proof of Theorem difexg
StepHypRef Expression
1 difss 4107 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 5219 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 686 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3495  cdif 3932  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-in 3942  df-ss 3951
This theorem is referenced by:  difexi  5224  difex2  7470  elpwun  7479  2oconcl  8119  fnoe  8126  ralxpmap  8449  difsnen  8588  domdifsn  8589  domunsncan  8606  fodomr  8657  domss2  8665  domssex2  8666  domssex  8667  mapdom2  8677  limenpsi  8681  sucdom2  8703  brwdom2  9026  infeq5i  9088  infdifsn  9109  dfac8clem  9447  acni  9460  infdif  9620  infpss  9628  ssfin4  9721  isf34lem1  9783  compssiso  9785  enfin1ai  9795  fin1a2lem7  9817  fin1a2lem13  9823  fpwwe2lem13  10053  fpwwe2  10054  canthp1lem1  10063  hashgt23el  13775  hashf1lem1  13803  brfi1indALT  13848  mrieqv2d  16900  mreexexlemd  16905  pmtrfv  18511  dpjidcl  19111  isirred  19380  isdrng2  19443  drngmcl  19446  drngid2  19449  isdrngd  19458  subdrgint  19513  cnmsubglem  20538  islindf4  20912  smadiadetlem1a  21202  basdif0  21491  tgdif0  21530  clsval2  21588  pnrmopn  21881  cmpcld  21940  cmpfi  21946  csdfil  22432  ufileu  22457  filufint  22458  alexsublem  22582  ptcmplem2  22591  bcth3  23863  iunmbl  24083  tdeglem4  24583  logbfval  25295  nbfusgrlevtxm2  27088  vtxdginducedm1  27253  frgrwopreglem1  28019  eigvecval  29601  elpwdifcl  30215  disjdifprg  30254  padct  30382  resf1o  30393  xrge00  30601  xrge0tsmsd  30620  tocycfv  30679  tocycf  30687  cyc3conja  30727  locfinref  31005  esummono  31213  esumpad  31214  esumpad2  31215  insiga  31296  ldsysgenld  31319  sigapildsys  31321  carsgclctun  31479  sitgclg  31500  ballotlemfrc  31684  ballotlem8  31694  bnj852  32093  bnj865  32095  subfacp1lem5  32329  iscvm  32404  cvmsval  32411  mdvval  32649  topdifinffinlem  34511  pibt2  34581  poimirlem15  34789  voliunnfl  34818  fdc  34903  isdrngo2  35119  selvval2lemn  39015  selvval2lem4  39016  selvval2lem5  39017  selvcl  39018  lzenom  39247  diophin  39249  diophren  39290  deg1mhm  39687  clcnvlem  39863  dssmapfv3d  40245  dssmapnvod  40246  ovolsplit  42154  stoweidlem57  42223  fourierdlem102  42374  fourierdlem114  42386  pwsal  42481  intsal  42494  gsumge0cl  42534  sge0ss  42575  sge0fodjrnlem  42579  iundjiunlem  42622  iundjiun  42623  meaiunlelem  42631  caragendifcl  42677  carageniuncllem1  42684  isomenndlem  42693  hoidmv1lelem2  42755  lincdifsn  44377  lindslinindsimp1  44410  lindslinindimp2lem2  44412  lindslinindimp2lem4  44414  lindslinindsimp2lem5  44415  lindslinindsimp2  44416  lincresunit1  44430  lincresunit2  44431  lincresunit3lem2  44433  lincresunit3  44434
  Copyright terms: Public domain W3C validator