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

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

Proof of Theorem difexg
StepHypRef Expression
1 difss 3715 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 4764 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 705 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Vcvv 3186  cdif 3552  wss 3555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3558  df-in 3562  df-ss 3569
This theorem is referenced by:  difexi  4769  difexOLD  4770  difex2  6918  elpwun  6924  2oconcl  7528  fnoe  7535  ralxpmap  7851  difsnen  7986  domdifsn  7987  domunsncan  8004  fodomr  8055  domss2  8063  domssex2  8064  domssex  8065  mapdom2  8075  limenpsi  8079  sucdom2  8100  findcard  8143  findcard2  8144  frfi  8149  unfilem3  8170  brwdom2  8422  infeq5i  8477  infdifsn  8498  dfac8clem  8799  acni  8812  dfac9  8902  dfacacn  8907  infpss  8983  ssfin4  9076  fin23lem28  9106  isf32lem6  9124  isf32lem7  9125  isf32lem8  9126  isf34lem1  9138  compssiso  9140  enfin1ai  9150  fin1a2lem7  9172  fin1a2lem13  9178  axdc2lem  9214  axcclem  9223  zornn0g  9271  fpwwe2lem13  9408  fpwwe2  9409  canthp1lem1  9418  grothprim  9600  hashbclem  13174  hashf1lem1  13177  fi1uzind  13218  brfi1uzind  13219  brfi1indALT  13221  opfi1uzind  13222  fi1uzindOLD  13224  brfi1uzindOLD  13225  brfi1indALTOLD  13227  opfi1uzindOLD  13228  ramub1lem1  15654  mrieqv2d  16220  mreexexlemd  16225  pltfval  16880  pmtrfv  17793  dpjidcl  18378  isirred  18620  isdrng2  18678  drngmcl  18681  drngid2  18684  isdrngd  18693  lssset  18853  xrs1mnd  19703  xrs1cmn  19705  xrge0subm  19706  cnmsubglem  19728  islindf4  20096  smadiadetlem1a  20388  basdif0  20668  tgdif0  20707  clsval2  20764  neitr  20894  lecldbas  20933  pnrmopn  21057  cmpcld  21115  cmpfi  21121  csdfil  21608  ufileu  21633  filufint  21634  alexsublem  21758  ptcmplem2  21767  xrge0gsumle  22544  xrge0tsms  22545  bcth3  23036  iunmbl  23228  i1fd  23354  tdeglem4  23724  reefgim  24108  logbmpt  24426  logbfval  24428  axlowdimlem15  25736  axlowdim  25741  elntg  25764  nbfusgrlevtxm1  26166  nbfusgrlevtxm2  26167  cusgrfilem3  26240  frgrwopreglem1  27039  eigvecval  28601  elpwdifcl  29202  disjdifprg  29230  padct  29337  resf1o  29345  xrge00  29468  xrge0tsmsd  29567  locfinref  29687  esummono  29894  esumpad  29895  esumpad2  29896  insiga  29978  ldsysgenld  30001  sigapildsys  30003  carsgclctun  30161  sitgclg  30182  ballotlemfrc  30366  ballotlem8  30376  bnj852  30696  bnj865  30698  subfacp1lem5  30871  iscvm  30946  cvmsval  30953  mdvval  31106  topdifinffinlem  32824  poimirlem15  33053  voliunnfl  33082  fdc  33170  isdrngo2  33386  watvalN  34756  hvmapfval  36525  lzenom  36810  diophin  36813  diophren  36854  cntzsdrg  37250  deg1mhm  37263  sssymdifcl  37355  clcnvlem  37408  dssmapfv3d  37792  dssmapnvod  37793  ovolsplit  39509  stoweidlem57  39578  fourierdlem102  39729  fourierdlem114  39741  pwsal  39839  intsal  39852  gsumge0cl  39892  sge0ss  39933  sge0fodjrnlem  39937  iundjiunlem  39980  iundjiun  39981  meaiunlelem  39989  caragendifcl  40032  carageniuncllem1  40039  isomenndlem  40048  hoidmv1lelem2  40110  lincdifsn  41498  lindslinindsimp1  41531  lindslinindimp2lem2  41533  lindslinindimp2lem4  41535  lindslinindsimp2lem5  41536  lindslinindsimp2  41537  lincresunit1  41551  lincresunit2  41552  lincresunit3lem2  41554  lincresunit3  41555
  Copyright terms: Public domain W3C validator