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

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

Proof of Theorem difexg
StepHypRef Expression
1 difss 3881 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 4957 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 708 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2140  Vcvv 3341  cdif 3713  wss 3716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-dif 3719  df-in 3723  df-ss 3730
This theorem is referenced by:  difexi  4962  difex2  7136  elpwun  7144  2oconcl  7755  fnoe  7762  ralxpmap  8076  difsnen  8210  domdifsn  8211  domunsncan  8228  fodomr  8279  domss2  8287  domssex2  8288  domssex  8289  mapdom2  8299  limenpsi  8303  sucdom2  8324  findcard  8367  findcard2  8368  frfi  8373  unfilem3  8394  brwdom2  8646  infeq5i  8709  infdifsn  8730  dfac8clem  9066  acni  9079  dfac9  9171  dfacacn  9176  infpss  9252  ssfin4  9345  fin23lem28  9375  isf32lem6  9393  isf32lem7  9394  isf32lem8  9395  isf34lem1  9407  compssiso  9409  enfin1ai  9419  fin1a2lem7  9441  fin1a2lem13  9447  axdc2lem  9483  axcclem  9492  zornn0g  9540  fpwwe2lem13  9677  fpwwe2  9678  canthp1lem1  9687  grothprim  9869  hashbclem  13449  hashf1lem1  13452  fi1uzind  13492  brfi1uzind  13493  brfi1indALT  13495  ramub1lem1  15953  mrieqv2d  16522  mreexexlemd  16527  pltfval  17181  pmtrfv  18093  dpjidcl  18678  isirred  18920  isdrng2  18980  drngmcl  18983  drngid2  18986  isdrngd  18995  lssset  19157  xrs1mnd  20007  xrs1cmn  20009  xrge0subm  20010  cnmsubglem  20032  islindf4  20400  smadiadetlem1a  20692  basdif0  20980  tgdif0  21019  clsval2  21077  neitr  21207  lecldbas  21246  pnrmopn  21370  cmpcld  21428  cmpfi  21434  csdfil  21920  ufileu  21945  filufint  21946  alexsublem  22070  ptcmplem2  22079  xrge0gsumle  22858  xrge0tsms  22859  bcth3  23349  iunmbl  23542  i1fd  23668  tdeglem4  24040  reefgim  24424  logbmpt  24747  logbfval  24749  axlowdimlem15  26057  axlowdim  26062  elntg  26085  nbfusgrlevtxm2  26500  cusgrfilem3  26585  vtxdginducedm1  26671  frgrwopreglem1  27488  eigvecval  29086  elpwdifcl  29687  disjdifprg  29717  padct  29828  resf1o  29836  xrge00  30017  xrge0tsmsd  30116  locfinref  30239  esummono  30447  esumpad  30448  esumpad2  30449  insiga  30531  ldsysgenld  30554  sigapildsys  30556  carsgclctun  30714  sitgclg  30735  ballotlemfrc  30919  ballotlem8  30929  bnj852  31320  bnj865  31322  subfacp1lem5  31495  iscvm  31570  cvmsval  31577  mdvval  31730  topdifinffinlem  33525  poimirlem15  33756  voliunnfl  33785  fdc  33873  isdrngo2  34089  watvalN  35801  hvmapfval  37569  lzenom  37854  diophin  37857  diophren  37898  cntzsdrg  38293  deg1mhm  38306  sssymdifcl  38398  clcnvlem  38451  dssmapfv3d  38834  dssmapnvod  38835  ovolsplit  40727  stoweidlem57  40796  fourierdlem102  40947  fourierdlem114  40959  pwsal  41057  intsal  41070  gsumge0cl  41110  sge0ss  41151  sge0fodjrnlem  41155  iundjiunlem  41198  iundjiun  41199  meaiunlelem  41207  caragendifcl  41253  carageniuncllem1  41260  isomenndlem  41269  hoidmv1lelem2  41331  lincdifsn  42742  lindslinindsimp1  42775  lindslinindimp2lem2  42777  lindslinindimp2lem4  42779  lindslinindsimp2lem5  42780  lindslinindsimp2  42781  lincresunit1  42795  lincresunit2  42796  lincresunit3lem2  42798  lincresunit3  42799
  Copyright terms: Public domain W3C validator