Theorem fmpttd 6971

Description: Version of fmptd 6970 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)

Hypothesis

Ref	Expression
fmpttd.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
fmpttd	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem fmpttd

Step	Hyp	Ref	Expression
1		fmpttd.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
2		eqid 2738	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fmptd 6970	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ↦ cmpt 5153  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  fmpt3d  6972  fliftrel  7159  pw2f1olem  8816  mapxpen  8879  fsuppmptif  9088  wdom2d  9269  cantnflem1d  9376  cantnflem1  9377  ac5num  9723  acni2  9733  infpwfien  9749  fin23lem39  10037  fin1a2lem12  10098  canthp1lem2  10340  wuncval2  10434  gruf  10498  monoord2  13682  seqf1o  13692  ccatcl  14205  swrdcl  14286  swrdwrdsymb  14303  revcl  14402  revlen  14403  ello1mpt  15158  lo1o12  15170  lo1eq  15205  rlimeq  15206  climmpt2  15210  climrecl  15220  climge0  15221  o1compt  15224  rlimcn1b  15226  rlimdiv  15285  isercoll2  15308  caurcvg2  15317  fsumf1o  15363  sumss  15364  fsumss  15365  fsumcl2lem  15371  fsumadd  15380  isumclim3  15399  isummulc2  15402  fsummulc2  15424  fsumrelem  15447  climfsum  15460  isumshft  15479  divcnv  15493  prodfdiv  15536  fprodf1o  15584  prodss  15585  fprodss  15586  fprodser  15587  fprodcl2lem  15588  fprodmul  15598  fproddiv  15599  fprodn0  15617  iprodclim3  15638  fprodefsum  15732  iserodd  16464  prmreclem2  16546  vdwapf  16601  vdwlem4  16613  ramcl  16658  prmodvdslcmf  16676  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  mrcflem  17232  mreacs  17284  acsfn  17285  hofcllem  17892  hofcl  17893  yonedalem3a  17908  yonedalem4c  17911  yonedainv  17915  prdspjmhm  18382  pwsco1mhm  18385  pwsco2mhm  18386  gsumz  18389  gsumwspan  18400  odf1o1  19092  odf1o2  19093  sylow2blem1  19140  mulgmhm  19344  mulgghm  19345  iscyggen2  19396  cyggenod  19399  iscyg3  19401  gsumzsplit  19443  gsumsplit2  19445  gsumconst  19450  gsummptshft  19452  gsummhm2  19455  gsummptmhm  19456  gsummptf1o  19479  gsum2dlem1  19486  gsum2dlem2  19487  gsum2d  19488  prdsgsum  19497  dprdfeq0  19540  dprdlub  19544  dprdz  19548  dprd2dlem1  19559  dprd2da  19560  srglmhm  19686  srgrmhm  19687  ringlghm  19758  ringrghm  19759  gsumdixp  19763  lmodvsghm  20099  gsumfsum  20577  regsumfsum  20578  expmhm  20579  expghm  20609  evpmodpmf1o  20713  frlmgsum  20889  frlmsplit2  20890  frlmphl  20898  uvcff  20908  uvcresum  20910  snifpsrbag  21035  psrass1lemOLD  21053  psrass1lem  21056  psrmulcllem  21066  psrlidm  21082  psrridm  21083  psrcom  21088  resspsrmul  21096  mvrf  21103  mplmon  21146  mplmonmul  21147  mplcoe1  21148  mplcoe5lem  21150  mplcoe5  21151  mplbas2  21153  psrbagsn  21181  evlslem4  21194  evlslem2  21199  evlslem3  21200  evlslem6  21201  evlslem1  21202  evlsval2  21207  psropprmul  21319  coe1mul2  21350  coe1tmmul2  21357  coe1tmmul  21358  ply1coe  21377  gsumsmonply1  21384  gsummoncoe1  21385  mamulid  21498  mamurid  21499  mdetunilem9  21677  mdetuni0  21678  mdetmul  21680  smadiadetlem3lem1  21723  m2cpmfo  21813  pmatcollpw1  21833  pmatcollpw3lem  21840  pmatcollpw3fi1lem2  21844  pm2mpcl  21854  mply1topmatcl  21862  mp2pm2mplem2  21864  mp2pm2mp  21868  pm2mpmhmlem2  21876  cayhamlem4  21945  pptbas  22066  tgrest  22218  resttopon  22220  rest0  22228  restfpw  22238  ordtbaslem  22247  ordtuni  22249  ordtrest  22261  cnpfval  22293  pnrmopn  22402  cncmp  22451  discmp  22457  1stcfb  22504  2ndcomap  22517  dis2ndc  22519  comppfsc  22591  kgencmp  22604  ptpjpre1  22630  ptpjcn  22670  ptcldmpt  22673  ptclsg  22674  dfac14  22677  xkoccn  22678  txcnp  22679  ptcnp  22681  uptx  22684  ptcn  22686  ptrescn  22698  xkoptsub  22713  xkoco1cn  22716  xkoco2cn  22717  cnmpt11  22722  pt1hmeo  22865  fbasrn  22943  trfilss  22948  trfg  22950  rnelfmlem  23011  flfcnp2  23066  fclscmpi  23088  alexsublem  23103  ptcmplem3  23113  symgtgp  23165  subgntr  23166  opnsubg  23167  clsnsg  23169  tgpconncomp  23172  eltsms  23192  haustsms  23195  tsmscls  23197  tsms0  23201  tsmsmhm  23205  tgptsmscls  23209  tsmssplit  23211  tsmsxplem1  23212  tsmsxplem2  23213  prdsdsf  23428  prdsxmetlem  23429  imasdsf1olem  23434  prdsbl  23553  stdbdxmet  23577  met1stc  23583  xrge0gsumle  23902  xrge0tsms  23903  cncfmpt2ss  23985  cnmptre  23996  evth  24028  evth2  24029  tcphcph  24306  rrxmval  24474  minveclem1  24493  minveclem3b  24497  iunmbl  24622  uniioombllem3  24654  ismbfcn2  24707  mbfeqalem1  24710  mbfeqalem2  24711  mbfss  24715  mbfmulc2re  24717  mbfneg  24719  mbfpos  24720  mbfposr  24721  mbfposb  24722  mbfadd  24730  mbfmulc2  24732  mbfsup  24733  mbfinf  24734  mbflimsup  24735  mbflimlem  24736  mbflim  24737  itg1climres  24784  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1flimlem  24792  mbfi1flim  24793  mbfmullem2  24794  mbfmul  24796  itg2const2  24811  itg2seq  24812  itg2monolem1  24820  itg2monolem2  24821  itg2monolem3  24822  itg2mono  24823  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  itg2cn  24833  iblss  24874  itgitg1  24878  itgle  24879  itgeqa  24883  itgss3  24884  ibladdlem  24889  itgaddlem1  24892  iblabslem  24897  iblabs  24898  iblabsr  24899  iblmulc2  24900  itgmulc2lem1  24901  bddmulibl  24908  bddiblnc  24911  itggt0  24913  itgcn  24914  ellimc2  24946  limcmpt  24952  limcres  24955  limccnp  24960  limccnp2  24961  limcco  24962  perfdvf  24972  dvcnp2  24989  dvaddbr  25007  dvmulbr  25008  dvcjbr  25018  dvexp  25022  dvrec  25024  dvmptres3  25025  dvmptadd  25029  dvmptmul  25030  dvmptres2  25031  dvmptcmul  25033  dvmptcj  25037  dvmptntr  25040  dvmptco  25041  dvcnvlem  25045  dvef  25049  dvferm1  25054  dvferm2  25056  rolle  25059  dvlipcn  25063  dvle  25076  dvivth  25079  lhop1lem  25082  lhop1  25083  lhop2  25084  lhop  25085  dvfsumle  25090  dvfsumge  25091  dvmptrecl  25093  dvfsumlem2  25096  itgsubstlem  25117  itgpowd  25119  tdeglem4  25129  tdeglem4OLD  25130  coe1mul3  25169  elply2  25262  plyf  25264  elplyd  25268  plypf1  25278  coeeq2  25308  coemullem  25316  coe1termlem  25324  dvply2g  25350  elqaalem2  25385  taylfvallem  25422  taylf  25425  tayl0  25426  taylpfval  25429  taylthlem1  25437  taylthlem2  25438  ulmcau  25459  ulmss  25461  ulmdvlem3  25466  mtest  25468  mtestbdd  25469  itgulm2  25473  dvradcnv  25485  pserulm  25486  pserdvlem2  25492  abelthlem9  25504  pige3ALT  25581  logtayl  25720  logccv  25723  loglesqrt  25816  leibpi  25997  rlimcnp  26020  rlimcnp2  26021  xrlimcnp  26023  efrlim  26024  dfef2  26025  o1cxp  26029  cxp2lim  26031  amgmlem  26044  lgamgulmlem2  26084  lgamgulmlem6  26088  lgamcvg2  26109  regamcl  26115  relgamcl  26116  basellem2  26136  basellem3  26137  sqff1o  26236  fsumvma  26266  dchrelbasd  26292  lgseisenlem3  26430  lgseisenlem4  26431  chpo1ub  26533  dchrisum0lem2a  26570  logsqvma2  26596  pnt2  26666  pnt  26667  incistruhgr  27352  minvecolem1  29137  hoaddcl  30021  homulcl  30022  cofmpt2  30870  fpwrelmap  30970  gsummpt2d  31211  xrge0tsmsd  31219  gsumvsca1  31381  gsumvsca2  31382  elrspunidl  31508  fedgmullem1  31612  fedgmullem2  31613  ordtrestNEW  31773  esumf1o  31918  esumadd  31925  esumcst  31931  esumpfinval  31943  esumpcvgval  31946  esumcvg  31954  esumsup  31957  measinb  32089  measdivcst  32092  sitgclg  32209  dstfrvclim1  32344  gsumncl  32419  gsumnunsn  32420  fdvneggt  32480  fdvnegge  32482  itgexpif  32486  logdivsqrle  32530  indispconn  33096  cvxpconn  33104  cvmsss2  33136  cvmliftlem6  33152  cvmliftlem8  33154  mrsubcv  33372  mrsubff  33374  mrsubrn  33375  mrsubccat  33380  elmrsubrn  33382  msubrn  33391  msubff  33392  divcnvlin  33604  faclimlem2  33616  faclim  33618  faclim2  33620  knoppcnlem5  34604  knoppcnlem8  34607  knoppcnlem10  34609  knoppcnlem11  34610  curf  35682  finixpnum  35689  matunitlindflem1  35700  matunitlindflem2  35701  ptrest  35703  poimirlem17  35721  poimirlem20  35724  poimirlem24  35728  poimirlem30  35734  broucube  35738  mblfinlem2  35742  volsupnfl  35749  mbfposadd  35751  itg2addnclem2  35756  itg2gt0cn  35759  ibladdnclem  35760  itgaddnclem1  35762  itgaddnc  35764  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  itgmulc2nclem1  35770  itgmulc2nclem2  35771  itgmulc2nc  35772  itgabsnc  35773  itggt0cn  35774  ftc1cnnc  35776  ftc1anclem1  35777  ftc1anclem2  35778  ftc1anclem3  35779  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  areacirclem4  35795  upixp  35814  totbndbnd  35874  prdsbnd  35878  cntotbnd  35881  rrnequiv  35920  lsatlss  36937  tendoplcl  38722  tendoicl  38737  aks4d1p1p5  40011  aks4d1p9  40024  sticksstones10  40039  sticksstones17  40047  sticksstones18  40048  pwspjmhmmgpd  40192  pwsgprod  40194  evlsval3  40195  evlsbagval  40198  fsuppind  40202  fsuppssind  40205  mhpind  40206  mhphflem  40207  mhphf  40208  cmpfiiin  40435  mzpclall  40465  mzpindd  40484  fphpdo  40555  dnnumch3  40788  kelac1  40804  dfac21  40807  rfovcnvf1od  41501  fsovfd  41509  fsovcnvlem  41510  clsk3nimkb  41539  mnringmulrcld  41735  expgrowth  41842  mptelpm  42601  mapss2  42634  monoord2xrv  42914  expcnfg  43022  clim1fr1  43032  sumnnodd  43061  limsupvaluz2  43169  supcnvlimsup  43171  climliminflimsupd  43232  liminfltlem  43235  cncfmptssg  43302  cncfcompt  43314  cxpcncf2  43330  dvsinax  43344  fperdvper  43350  dvcosax  43357  dvnmptdivc  43369  dvnprodlem2  43378  dvnprodlem3  43379  iblsplit  43397  itgcoscmulx  43400  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  dirkerf  43528  dirkeritg  43533  hoidmvlelem1  44023  hoidmvlelem5  44027  ovnhoilem1  44029  ovnhoilem2  44030  ovnlecvr2  44038  ovncvr2  44039  hoidifhspf  44046  hspmbllem2  44055  opnvonmbllem2  44061  iccvonmbllem  44106  vonioolem1  44108  vonioolem2  44109  vonicclem1  44111  vonicclem2  44112  smfid  44175  cfsetsnfsetf  44439  funcringcsetcALTV2lem3  45484  funcringcsetclem3ALTV  45507  gsumlsscl  45607  ply1mulgsum  45619  lincfsuppcl  45642  linccl  45643  lincsum  45658  lincscmcl  45661  lcoss  45665  lincext1  45683  el0ldep  45695  lincresunit1  45706  lincresunit3  45710  lmod1zr  45722  fdivmptf  45775  refdivmptf  45776  1arymaptf  45875  aacllem  46391  amgmwlem  46392