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

Theorem difexd 5331
Description: Existence of a difference. (Contributed by SN, 16-Jul-2024.)
Hypothesis
Ref Expression
difexd.1 (𝜑𝐴𝑉)
Assertion
Ref Expression
difexd (𝜑 → (𝐴𝐵) ∈ V)

Proof of Theorem difexd
StepHypRef Expression
1 difexd.1 . 2 (𝜑𝐴𝑉)
2 difexg 5329 . 2 (𝐴𝑉 → (𝐴𝐵) ∈ V)
31, 2syl 17 1 (𝜑 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  Vcvv 3480  cdif 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968
This theorem is referenced by:  sexp2  8171  sexp3  8178  ralxpmap  8936  domdifsn  9094  domunsncan  9112  mapdom2  9188  acni  10085  infdif  10248  infpss  10256  enfin1ai  10424  fpwwe2  10683  canthp1lem1  10692  hashf1lem1  14494  mrieqv2d  17682  mreexexlemd  17687  dpjidcl  20078  pnrmopn  23351  cmpfi  23416  csdfil  23902  ufileu  23927  filufint  23928  alexsublem  24052  bcth3  25365  iunmbl  25588  tdeglem4  26099  fdifsupp  32694  gsummptres2  33056  tocycfv  33129  cyc3conja  33177  rprmdvdsprod  33562  esummono  34055  esumpad  34056  esumpad2  34057  insiga  34138  selvcllemh  42590  selvcllem4  42591  selvcllem5  42592  selvcl  42593  selvval2  42594  selvvvval  42595  selvadd  42598  selvmul  42599  fsuppssind  42603  tfsconcatun  43350  oaun2  43394  oaun3  43395  clcnvlem  43636  dssmapfv3d  44032  dssmapnvod  44033  ovolsplit  46003  intsal  46345  sge0ss  46427  sge0fodjrnlem  46431  iundjiun  46475  meaiunlelem  46483  iscnrm3rlem7  48843
  Copyright terms: Public domain W3C validator