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

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

Proof of Theorem difexg
StepHypRef Expression
1 difss 4062 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 5194 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 689 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Vcvv 3444  cdif 3881  wss 3884
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-sep 5170
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-v 3446  df-dif 3887  df-in 3891  df-ss 3901
This theorem is referenced by:  difexi  5199  difex2  7466  elpwun  7475  2oconcl  8115  fnoe  8122  ralxpmap  8447  difsnen  8586  domdifsn  8587  domunsncan  8604  sucdom2  8614  fodomr  8656  domss2  8664  domssex2  8665  domssex  8666  mapdom2  8676  limenpsi  8680  brwdom2  9025  infeq5i  9087  infdifsn  9108  dfac8clem  9447  acni  9460  infdif  9624  infpss  9632  ssfin4  9725  isf34lem1  9787  compssiso  9789  enfin1ai  9799  fin1a2lem7  9821  fin1a2lem13  9827  fpwwe2lem13  10057  fpwwe2  10058  canthp1lem1  10067  hashgt23el  13785  hashf1lem1  13813  mrieqv2d  16905  mreexexlemd  16910  pmtrfv  18575  dpjidcl  19176  isirred  19448  isdrng2  19508  drngmcl  19511  drngid2  19514  isdrngd  19523  subdrgint  19578  cnmsubglem  20157  islindf4  20530  smadiadetlem1a  21271  basdif0  21561  tgdif0  21600  clsval2  21658  pnrmopn  21951  cmpcld  22010  cmpfi  22016  csdfil  22502  ufileu  22527  filufint  22528  alexsublem  22652  ptcmplem2  22661  bcth3  23938  iunmbl  24160  tdeglem4  24664  logbfval  25379  nbfusgrlevtxm2  27171  vtxdginducedm1  27336  frgrwopreglem1  28100  eigvecval  29682  elpwdifcl  30302  disjdifprg  30341  padct  30484  resf1o  30495  xrge00  30723  gsummptres2  30741  xrge0tsmsd  30745  tocycfv  30804  tocycf  30812  cyc3conja  30852  ist0cld  31186  locfinref  31194  esummono  31421  esumpad  31422  esumpad2  31423  insiga  31504  ldsysgenld  31527  sigapildsys  31529  carsgclctun  31687  sitgclg  31708  ballotlemfrc  31892  ballotlem8  31902  bnj852  32301  bnj865  32303  subfacp1lem5  32539  iscvm  32614  cvmsval  32621  mdvval  32859  topdifinffinlem  34759  pibt2  34829  poimirlem15  35065  voliunnfl  35094  fdc  35176  isdrngo2  35389  difexd  39391  selvval2lemn  39417  selvval2lem4  39418  selvval2lem5  39419  selvcl  39420  lzenom  39698  diophin  39700  diophren  39741  deg1mhm  40138  clcnvlem  40310  dssmapfv3d  40707  dssmapnvod  40708  ovolsplit  42617  stoweidlem57  42686  fourierdlem102  42837  fourierdlem114  42849  pwsal  42944  intsal  42957  gsumge0cl  42997  sge0ss  43038  sge0fodjrnlem  43042  iundjiun  43086  meaiunlelem  43094  caragendifcl  43140  carageniuncllem1  43147  isomenndlem  43156  hoidmv1lelem2  43218  lincdifsn  44820  lindslinindsimp1  44853  lindslinindimp2lem2  44855  lindslinindimp2lem4  44857  lindslinindsimp2lem5  44858  lindslinindsimp2  44859  lincresunit1  44873  lincresunit2  44874  lincresunit3lem2  44876  lincresunit3  44877
  Copyright terms: Public domain W3C validator