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

Theorem mptexd 6978
Description: If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 6975. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypothesis
Ref Expression
mptexd.1 (𝜑𝐴𝑉)
Assertion
Ref Expression
mptexd (𝜑 → (𝑥𝐴𝐵) ∈ V)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem mptexd
StepHypRef Expression
1 mptexd.1 . 2 (𝜑𝐴𝑉)
2 mptexg 6975 . 2 (𝐴𝑉 → (𝑥𝐴𝐵) ∈ V)
31, 2syl 17 1 (𝜑 → (𝑥𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3492  cmpt 5137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356
This theorem is referenced by:  mptsuppdifd  7841  mpocurryvald  7925  fsuppmptif  8851  sniffsupp  8861  cantnfrescl  9127  cantnflem1  9140  infxpenc2lem2  9434  ac5num  9450  ac6num  9889  negfi  11577  seqof2  13416  ramcl  16353  prdsplusgval  16734  prdsmulrval  16736  prdsvscaval  16740  galactghm  18461  gsum2dlem2  19020  gsum2d  19021  dprdfinv  19070  dprdfadd  19071  dmdprdsplitlem  19088  dpjfval  19106  dpjidcl  19109  mptscmfsupp0  19628  psrass1lem  20085  psrridm  20112  psrcom  20117  mvrfval  20128  mplcoe5  20177  mplbas2  20179  evlslem6  20222  selvffval  20257  evls1sca  20414  frlmgsum  20844  frlmphllem  20852  matgsum  20974  mvmulval  21080  mavmul0g  21090  marepvval0  21103  ptcnplem  22157  xkocnv  22350  ptcmplem3  22590  prdsdsf  22904  ressprdsds  22908  prdsxmslem2  23066  rrx0  23927  tdeglem4  24581  pserulm  24937  efsubm  25062  suppovss  30354  fsuppcurry1  30387  fsuppcurry2  30388  tocycval  30677  rmfsupp2  30793  drgextgsum  30896  fedgmullem2  30925  ofcfval  31256  lpadval  31846  bj-imdirval  34364  rfovfvd  40226  fsovfvd  40234  dssmapf1od  40245  choicefi  41339  axccdom  41363  climeldmeqmpt  41825  climfveqmpt  41828  climfveqmpt3  41839  climeldmeqmpt3  41846  climfveqmpt2  41850  climeldmeqmpt2  41852  climeqmpt  41854  limsupresicompt  41913  liminfresicompt  41937  liminfvalxr  41940  liminflbuz2  41972  iccvonmbllem  42837  vonioolem1  42839  vonioolem2  42840  vonicclem1  42842  vonicclem2  42843  smflimmpt  42961  smflimsuplem6  42976  fundcmpsurbijinjpreimafv  43444  prproropen  43547  uspgrbispr  43903
  Copyright terms: Public domain W3C validator