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

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

Proof of Theorem difexg
StepHypRef Expression
1 difss 3880 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 4956 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 708 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  Vcvv 3340  cdif 3712  wss 3715
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 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933
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 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-in 3722  df-ss 3729
This theorem is referenced by:  difexi  4961  difex2  7134  elpwun  7142  2oconcl  7752  fnoe  7759  ralxpmap  8073  difsnen  8207  domdifsn  8208  domunsncan  8225  fodomr  8276  domss2  8284  domssex2  8285  domssex  8286  mapdom2  8296  limenpsi  8300  sucdom2  8321  findcard  8364  findcard2  8365  frfi  8370  unfilem3  8391  brwdom2  8643  infeq5i  8706  infdifsn  8727  dfac8clem  9045  acni  9058  dfac9  9150  dfacacn  9155  infpss  9231  ssfin4  9324  fin23lem28  9354  isf32lem6  9372  isf32lem7  9373  isf32lem8  9374  isf34lem1  9386  compssiso  9388  enfin1ai  9398  fin1a2lem7  9420  fin1a2lem13  9426  axdc2lem  9462  axcclem  9471  zornn0g  9519  fpwwe2lem13  9656  fpwwe2  9657  canthp1lem1  9666  grothprim  9848  hashbclem  13428  hashf1lem1  13431  fi1uzind  13471  brfi1uzind  13472  brfi1indALT  13474  ramub1lem1  15932  mrieqv2d  16501  mreexexlemd  16506  pltfval  17160  pmtrfv  18072  dpjidcl  18657  isirred  18899  isdrng2  18959  drngmcl  18962  drngid2  18965  isdrngd  18974  lssset  19136  xrs1mnd  19986  xrs1cmn  19988  xrge0subm  19989  cnmsubglem  20011  islindf4  20379  smadiadetlem1a  20671  basdif0  20959  tgdif0  20998  clsval2  21056  neitr  21186  lecldbas  21225  pnrmopn  21349  cmpcld  21407  cmpfi  21413  csdfil  21899  ufileu  21924  filufint  21925  alexsublem  22049  ptcmplem2  22058  xrge0gsumle  22837  xrge0tsms  22838  bcth3  23328  iunmbl  23521  i1fd  23647  tdeglem4  24019  reefgim  24403  logbmpt  24725  logbfval  24727  axlowdimlem15  26035  axlowdim  26040  elntg  26063  nbfusgrlevtxm2  26478  cusgrfilem3  26563  vtxdginducedm1  26649  frgrwopreglem1  27466  eigvecval  29064  elpwdifcl  29665  disjdifprg  29695  padct  29806  resf1o  29814  xrge00  29995  xrge0tsmsd  30094  locfinref  30217  esummono  30425  esumpad  30426  esumpad2  30427  insiga  30509  ldsysgenld  30532  sigapildsys  30534  carsgclctun  30692  sitgclg  30713  ballotlemfrc  30897  ballotlem8  30907  bnj852  31298  bnj865  31300  subfacp1lem5  31473  iscvm  31548  cvmsval  31555  mdvval  31708  topdifinffinlem  33506  poimirlem15  33737  voliunnfl  33766  fdc  33854  isdrngo2  34070  watvalN  35782  hvmapfval  37550  lzenom  37835  diophin  37838  diophren  37879  cntzsdrg  38274  deg1mhm  38287  sssymdifcl  38379  clcnvlem  38432  dssmapfv3d  38815  dssmapnvod  38816  ovolsplit  40708  stoweidlem57  40777  fourierdlem102  40928  fourierdlem114  40940  pwsal  41038  intsal  41051  gsumge0cl  41091  sge0ss  41132  sge0fodjrnlem  41136  iundjiunlem  41179  iundjiun  41180  meaiunlelem  41188  caragendifcl  41234  carageniuncllem1  41241  isomenndlem  41250  hoidmv1lelem2  41312  lincdifsn  42723  lindslinindsimp1  42756  lindslinindimp2lem2  42758  lindslinindimp2lem4  42760  lindslinindsimp2lem5  42761  lindslinindsimp2  42762  lincresunit1  42776  lincresunit2  42777  lincresunit3lem2  42779  lincresunit3  42780
  Copyright terms: Public domain W3C validator