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

Theorem mptexd 7179
Description: If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7176. (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 7176 . 2 (𝐴𝑉 → (𝑥𝐴𝐵) ∈ V)
31, 2syl 17 1 (𝜑 → (𝑥𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3448  cmpt 5193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509
This theorem is referenced by:  mptsuppdifd  8122  mpocurryvald  8206  fsetfocdm  8806  fsuppmptif  9342  sniffsupp  9343  cantnfrescl  9619  cantnflem1  9632  infxpenc2lem2  9963  ac5num  9979  ac6num  10422  negfi  12111  seqof2  13973  ramcl  16908  prdsplusgval  17362  prdsmulrval  17364  prdsvscaval  17368  galactghm  19193  gsum2dlem2  19755  gsum2d  19756  dprdfinv  19805  dprdfadd  19806  dmdprdsplitlem  19823  dpjfval  19841  dpjidcl  19844  mptscmfsupp0  20403  frlmgsum  21194  frlmphllem  21202  psrass1lemOLD  21358  psrass1lem  21361  psrridm  21389  psrcom  21394  mvrfval  21405  mplcoe5  21457  mplbas2  21459  evlslem6  21507  selvffval  21542  evls1sca  21705  matgsum  21802  mvmulval  21908  mavmul0g  21918  marepvval0  21931  ptcnplem  22988  xkocnv  23181  ptcmplem3  23421  prdsdsf  23736  ressprdsds  23740  prdsxmslem2  23901  rrx0  24777  tdeglem4  25440  tdeglem4OLD  25441  pserulm  25797  efsubm  25923  addsunif  27332  suppovss  31640  fsuppcurry1  31684  fsuppcurry2  31685  gsummptres2  31937  tocycval  31999  rmfsupp2  32115  elrsp  32202  elrspunidl  32243  evls1fpws  32311  drgextgsum  32336  fedgmullem2  32365  minplyval  32412  ofcfval  32737  lpadval  33329  bj-imdirvallem  35680  sticksstones4  40586  sticksstones11  40593  sticksstones12a  40594  sticksstones12  40595  sticksstones17  40600  sticksstones18  40601  sticksstones19  40602  sticksstones20  40603  evlsbagval  40777  mhphf  40800  rfovfvd  42348  fsovfvd  42356  dssmapf1od  42367  choicefi  43495  axccdom  43517  climeldmeqmpt  43983  climfveqmpt  43986  climfveqmpt3  43997  climeldmeqmpt3  44004  climfveqmpt2  44008  climeldmeqmpt2  44010  climeqmpt  44012  limsupresicompt  44071  liminfresicompt  44095  liminfvalxr  44098  liminflbuz2  44130  iccvonmbllem  44993  vonioolem1  44995  vonioolem2  44996  vonicclem1  44998  vonicclem2  44999  smflimmpt  45125  smflimsuplem6  45140  cfsetsnfsetfv  45365  cfsetsnfsetf  45366  fundcmpsurbijinjpreimafv  45673  prproropen  45774  uspgrbispr  46127  1arymaptfv  46800  1arymaptfo  46803
  Copyright terms: Public domain W3C validator