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

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

Proof of Theorem difexg
StepHypRef Expression
1 difss 4091 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 5280 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 688 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  Vcvv 3445  cdif 3907  wss 3910
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-dif 3913  df-in 3917  df-ss 3927
This theorem is referenced by:  difexi  5285  difexd  5286  difex2  7693  elpwun  7702  2oconcl  8448  fnoe  8455  difsnen  8996  sucdom2OLD  9025  fodomr  9071  domss2  9079  domssex2  9080  domssex  9081  limenpsi  9095  dif1enlem  9099  sucdom2  9149  brwdom2  9508  infeq5i  9571  infdifsn  9592  dfac8clem  9967  ssfin4  10245  isf34lem1  10307  compssiso  10309  fin1a2lem7  10341  fin1a2lem13  10347  fpwwe2lem12  10577  hashgt23el  14323  hashf1lem1OLD  14353  pmtrfv  19232  isirred  20126  isdrng2  20196  drngmcl  20199  drngid2  20202  isdrngd  20212  subdrgint  20268  cnmsubglem  20858  islindf4  21242  smadiadetlem1a  22010  basdif0  22301  tgdif0  22340  clsval2  22399  cmpcld  22751  ptcmplem2  23402  iunmbl  24915  tdeglem4OLD  25423  logbfval  26138  nbfusgrlevtxm2  28273  vtxdginducedm1  28438  frgrwopreglem1  29203  eigvecval  30785  elpwdifcl  31401  disjdifprg  31440  padct  31580  resf1o  31591  xrge00  31821  xrge0tsmsd  31843  tocycf  31910  ist0cld  32354  locfinref  32362  ldsysgenld  32699  sigapildsys  32701  carsgclctun  32861  sitgclg  32882  ballotlemfrc  33066  ballotlem8  33076  bnj852  33473  bnj865  33475  subfacp1lem5  33718  iscvm  33793  cvmsval  33800  mdvval  34038  topdifinffinlem  35808  pibt2  35878  poimirlem15  36083  voliunnfl  36112  fdc  36194  isdrngo2  36407  lzenom  41070  diophin  41072  diophren  41113  deg1mhm  41511  stoweidlem57  44269  fourierdlem102  44420  fourierdlem114  44432  pwsal  44527  gsumge0cl  44583  caragendifcl  44726  carageniuncllem1  44733  isomenndlem  44742  hoidmv1lelem2  44804  lincdifsn  46476  lindslinindsimp1  46509  lindslinindimp2lem2  46511  lindslinindimp2lem4  46513  lindslinindsimp2lem5  46514  lindslinindsimp2  46515  lincresunit1  46529  lincresunit2  46530  lincresunit3lem2  46532  lincresunit3  46533
  Copyright terms: Public domain W3C validator