Theorem fmpttd 7100

Description: Version of fmptd 7099 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 2765	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fmptd 7099	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145   ↦ cmpt 5186  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  fmpt3d  7101  fliftrel  7296  fsetfocdm  8846  pw2f1olem  9057  mapxpen  9119  fsuppssov1  9332  fsuppmptif  9347  wdom2d  9530  cantnflem1d  9645  cantnflem1  9646  ac5num  10008  acni2  10018  infpwfien  10034  fin23lem39  10322  fin1a2lem12  10383  canthp1lem2  10626  wuncval2  10720  gruf  10784  monoord2  14060  seqf1o  14070  ccatcl  14601  swrdcl  14673  swrdwrdsymb  14690  revcl  14788  revlen  14789  ello1mpt  15562  lo1o12  15574  lo1eq  15609  rlimeq  15610  climmpt2  15614  climrecl  15624  climge0  15625  o1compt  15628  rlimcn1b  15630  rlimdiv  15687  isercoll2  15710  caurcvg2  15719  fsumf1o  15764  sumss  15765  fsumss  15766  fsumcl2lem  15772  fsumadd  15781  isumclim3  15800  isummulc2  15803  fsummulc2  15825  fsumrelem  15849  climfsum  15862  isumshft  15883  divcnv  15897  prodfdiv  15940  fprodf1o  15990  prodss  15991  fprodss  15992  fprodser  15993  fprodcl2lem  15994  fprodmul  16004  fproddiv  16005  fprodn0  16023  iprodclim3  16044  fprodefsum  16139  iserodd  16885  prmreclem2  16967  vdwapf  17022  vdwlem4  17034  ramcl  17079  prmodvdslcmf  17097  prdsplusg  17501  prdsmulr  17502  prdsvsca  17503  mrcflem  17652  mreacs  17704  acsfn  17705  hofcllem  18304  hofcl  18305  yonedalem3a  18320  yonedalem4c  18323  yonedainv  18327  prdspjmhm  18878  pwsco1mhm  18881  pwsco2mhm  18882  gsumz  18885  gsumwspan  18895  smndex1gbas  18951  odf1o1  19633  odf1o2  19634  sylow2blem1  19681  mulgmhm  19888  mulgghm  19889  iscyggen2  19942  cyggenod  19945  iscyg3  19947  gsumzsplit  19988  gsumsplit2  19990  gsumconst  19995  gsummptshft  19997  gsummhm2  20000  gsummptmhm  20001  gsummptf1o  20024  gsum2dlem1  20031  gsum2dlem2  20032  gsum2d  20033  prdsgsum  20042  dprdfeq0  20085  dprdlub  20089  dprdz  20093  dprd2dlem1  20104  dprd2da  20105  srglmhm  20294  srgrmhm  20295  ringlghm  20386  ringrghm  20387  gsumdixp  20391  pwspjmhmmgpd  20400  pwsgprod  20402  lmodvsghm  21013  gsumfsum  21544  regsumfsum  21545  expmhm  21546  expghm  21585  evpmodpmf1o  21706  frlmgsum  21882  frlmsplit2  21883  frlmphl  21891  uvcff  21901  uvcresum  21903  snifpsrbag  22030  psrass1lem  22043  rhmpsrlem1  22050  rhmpsrlem2  22051  psrmulcllem  22055  psrlidm  22071  psrridm  22072  psrcom  22077  resspsrmul  22085  mvrf  22094  mplmon  22146  mplmonmul  22147  mplcoe1  22148  mplcoe5lem  22150  mplcoe5  22151  mplbas2  22153  psrbagsn  22174  evlslem4  22187  evlslem2  22190  evlslem3  22191  evlslem6  22192  evlslem1  22193  evlsval2  22198  evlsval3  22200  evlsvvvallem  22202  evlsvvval  22204  selvvvval  22253  psdcl  22284  psdmplcl  22285  psdmul  22289  psropprmul  22357  coe1mul2  22390  coe1tmmul2  22397  coe1tmmul  22398  ply1coe  22419  gsumsmonply1  22428  gsummoncoe1  22429  mamulid  22559  mamurid  22560  mdetunilem9  22738  mdetuni0  22739  mdetmul  22741  smadiadetlem3lem1  22784  m2cpmfo  22874  pmatcollpw1  22894  pmatcollpw3lem  22901  pmatcollpw3fi1lem2  22905  pm2mpcl  22915  mply1topmatcl  22923  mp2pm2mplem2  22925  mp2pm2mp  22929  pm2mpmhmlem2  22937  cayhamlem4  23006  pptbas  23126  tgrest  23277  resttopon  23279  rest0  23287  restfpw  23297  ordtbaslem  23306  ordtuni  23308  ordtrest  23320  cnpfval  23352  pnrmopn  23461  cncmp  23510  discmp  23516  1stcfb  23563  2ndcomap  23576  dis2ndc  23578  comppfsc  23650  kgencmp  23663  ptpjpre1  23689  ptpjcn  23729  ptcldmpt  23732  ptclsg  23733  dfac14  23736  xkoccn  23737  txcnp  23738  ptcnp  23740  uptx  23743  ptcn  23745  ptrescn  23757  xkoptsub  23772  xkoco1cn  23775  xkoco2cn  23776  cnmpt11  23781  pt1hmeo  23924  fbasrn  24002  trfilss  24007  trfg  24009  rnelfmlem  24070  flfcnp2  24125  fclscmpi  24147  alexsublem  24162  ptcmplem3  24172  symgtgp  24224  subgntr  24225  opnsubg  24226  clsnsg  24228  tgpconncomp  24231  eltsms  24251  haustsms  24254  tsmscls  24256  tsms0  24260  tsmsmhm  24264  tgptsmscls  24268  tsmssplit  24270  tsmsxplem1  24271  tsmsxplem2  24272  prdsdsf  24485  prdsxmetlem  24486  imasdsf1olem  24491  prdsbl  24609  stdbdxmet  24633  met1stc  24639  xrge0gsumle  24952  xrge0tsms  24953  cncfmpt2ss  25036  cnmptre  25047  evth  25079  evth2  25080  tcphcph  25357  rrxmval  25525  minveclem1  25544  minveclem3b  25548  iunmbl  25673  uniioombllem3  25705  ismbfcn2  25758  mbfeqalem1  25761  mbfeqalem2  25762  mbfss  25766  mbfmulc2re  25768  mbfneg  25770  mbfpos  25771  mbfposr  25772  mbfposb  25773  mbfadd  25781  mbfmulc2  25783  mbfsup  25784  mbfinf  25785  mbflimsup  25786  mbflimlem  25787  mbflim  25788  itg1climres  25834  mbfi1fseqlem3  25837  mbfi1fseqlem4  25838  mbfi1flimlem  25842  mbfi1flim  25843  mbfmullem2  25844  mbfmul  25846  itg2const2  25861  itg2seq  25862  itg2monolem1  25870  itg2monolem2  25871  itg2monolem3  25872  itg2mono  25873  itg2gt0  25880  itg2cnlem1  25881  itg2cnlem2  25882  itg2cn  25883  iblss  25925  itgitg1  25929  itgle  25930  itgeqa  25934  itgss3  25935  ibladdlem  25940  itgaddlem1  25943  iblabslem  25948  iblabs  25949  iblabsr  25950  iblmulc2  25951  itgmulc2lem1  25952  bddmulibl  25959  bddiblnc  25962  itggt0  25964  itgcn  25965  ellimc2  25997  limcmpt  26003  limcres  26006  limccnp  26011  limccnp2  26012  limcco  26013  perfdvf  26023  dvcnp2  26040  dvaddbr  26058  dvmulbr  26059  dvcjbr  26069  dvexp  26073  dvrec  26075  dvmptres3  26076  dvmptadd  26080  dvmptmul  26081  dvmptres2  26082  dvmptcmul  26084  dvmptcj  26088  dvmptntr  26091  dvmptco  26092  dvcnvlem  26096  dvef  26100  dvferm1  26105  dvferm2  26107  rolle  26110  dvlipcn  26114  dvle  26127  dvivth  26130  lhop1lem  26133  lhop1  26134  lhop2  26135  lhop  26136  dvfsumle  26141  dvfsumge  26142  dvmptrecl  26144  dvfsumlem2  26147  itgsubstlem  26168  itgpowd  26170  tdeglem4  26178  coe1mul3  26217  elply2  26314  plyf  26316  elplyd  26320  plypf1  26330  coeeq2  26360  coemullem  26368  coe1termlem  26376  dvply2g  26407  elqaalem2  26442  taylfvallem  26479  taylf  26482  tayl0  26483  taylpfval  26486  taylthlem1  26494  taylthlem2  26495  ulmcau  26516  ulmss  26518  ulmdvlem3  26523  mtest  26525  mtestbdd  26526  itgulm2  26530  dvradcnv  26542  pserulm  26543  pserdvlem2  26549  abelthlem9  26561  pige3ALT  26643  logtayl  26783  logccv  26786  loglesqrt  26884  leibpi  27065  rlimcnp  27088  rlimcnp2  27089  xrlimcnp  27091  efrlim  27092  dfef2  27093  o1cxp  27097  cxp2lim  27099  amgmlem  27112  lgamgulmlem2  27152  lgamgulmlem6  27156  lgamcvg2  27177  regamcl  27183  relgamcl  27184  basellem2  27204  basellem3  27205  sqff1o  27304  fsumvma  27335  dchrelbasd  27361  lgseisenlem3  27499  lgseisenlem4  27500  chpo1ub  27602  dchrisum0lem2a  27639  logsqvma2  27665  pnt2  27735  pnt  27736  incistruhgr  29338  minvecolem1  31135  hoaddcl  32019  homulcl  32020  cofmpt2  32891  mptiffisupp  32950  fpwrelmap  32990  gsummpt2d  33282  gsummptfsres  33287  gsummptf1od  33288  gsummptfsf1o  33293  gsumfs2d  33294  gsumzrsum  33298  gsummulsubdishift2  33302  gsummulsubdishift1s  33303  gsummulsubdishift2s  33304  xrge0tsmsd  33306  gsumwrd2dccat  33311  gsumvsca1  33459  gsumvsca2  33460  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnlem3  33477  elrgspnlem4  33478  elrgspn  33479  elrgspnsubrunlem2  33481  elrspunidl  33652  elrspunsn  33653  ressply1evls1  33772  evl1deg2  33784  deg1prod  33790  selvascl  33824  selvply1rhmlem1  33827  extvfvcl  33843  evlextv  33849  mplvrpmga  33852  psrgsum  33855  psrmon  33856  psrmonmul  33857  psrmonprod  33859  esplyfvaln  33881  vietadeg1  33885  fedgmullem1  33936  fedgmullem2  33937  evls1fldgencl  33977  fldextrspunlsplem  33980  fldextrspunlsp  33981  extdgfialglem2  34000  ordtrestNEW  34228  esumf1o  34357  esumadd  34364  esumcst  34370  esumpfinval  34382  esumpcvgval  34385  esumcvg  34393  esumsup  34396  measinb  34528  measdivcst  34531  sitgclg  34649  dstfrvclim1  34785  gsumncl  34847  gsumnunsn  34848  fdvneggt  34904  fdvnegge  34906  itgexpif  34910  logdivsqrle  34954  indispconn  35597  cvxpconn  35605  cvmsss2  35637  cvmliftlem6  35653  cvmliftlem8  35655  mrsubcv  35873  mrsubff  35875  mrsubrn  35876  mrsubccat  35881  elmrsubrn  35883  msubrn  35892  msubff  35893  divcnvlin  36096  faclimlem2  36107  faclim  36109  faclim2  36111  knoppcnlem5  36948  knoppcnlem8  36951  knoppcnlem10  36953  knoppcnlem11  36954  curf  38109  finixpnum  38116  matunitlindflem1  38127  matunitlindflem2  38128  ptrest  38130  poimirlem17  38148  poimirlem20  38151  poimirlem24  38155  poimirlem30  38161  broucube  38165  mblfinlem2  38169  volsupnfl  38176  mbfposadd  38178  itg2addnclem2  38183  itg2gt0cn  38186  ibladdnclem  38187  itgaddnclem1  38189  itgaddnc  38191  iblabsnclem  38194  iblabsnc  38195  iblmulc2nc  38196  itgmulc2nclem1  38197  itgmulc2nclem2  38198  itgmulc2nc  38199  itgabsnc  38200  itggt0cn  38201  ftc1cnnc  38203  ftc1anclem1  38204  ftc1anclem2  38205  ftc1anclem3  38206  ftc1anclem4  38207  ftc1anclem5  38208  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  areacirclem4  38222  upixp  38240  totbndbnd  38300  prdsbnd  38304  cntotbnd  38307  rrnequiv  38346  lsatlss  39632  tendoplcl  41417  tendoicl  41432  aks4d1p1p5  42704  aks4d1p9  42717  hashscontpow  42751  sticksstones10  42784  sticksstones17  42792  sticksstones18  42793  unitscyglem1  42824  redvmptabs  42981  fimgmcyc  43164  evlsbagval  43180  evlselv  43183  fsuppind  43184  fsuppssind  43187  mhpind  43188  evlsmhpvvval  43189  mhphflem  43190  cmpfiiin  43290  mzpclall  43320  mzpindd  43339  fphpdo  43406  dnnumch3  43636  kelac1  43652  dfac21  43655  cantnfresb  43913  cantnf2  43914  tfsconcatrev  43937  rfovcnvf1od  44592  fsovfd  44600  fsovcnvlem  44601  clsk3nimkb  44628  mnringmulrcld  44816  expgrowth  44909  mptelpm  45752  mapss2  45780  monoord2xrv  46055  expcnfg  46165  clim1fr1  46175  sumnnodd  46204  limsupvaluz2  46310  supcnvlimsup  46312  climliminflimsupd  46373  liminfltlem  46376  cncfmptssg  46443  cncfcompt  46455  cxpcncf2  46471  dvsinax  46485  fperdvper  46491  dvcosax  46498  dvnmptdivc  46510  dvnprodlem2  46519  dvnprodlem3  46520  iblsplit  46538  itgcoscmulx  46541  itgiccshift  46552  itgperiod  46553  itgsbtaddcnst  46554  dirkerf  46669  dirkeritg  46674  hoidmvlelem1  47167  hoidmvlelem5  47171  ovnhoilem1  47173  ovnhoilem2  47174  ovnlecvr2  47182  ovncvr2  47183  hoidifhspf  47190  hspmbllem2  47199  opnvonmbllem2  47205  iccvonmbllem  47250  vonioolem1  47252  vonioolem2  47253  vonicclem1  47255  vonicclem2  47256  smfid  47324  cfsetsnfsetf  47650  funcringcsetcALTV2lem3  48912  funcringcsetclem3ALTV  48935  gsumlsscl  49011  ply1mulgsum  49021  lincfsuppcl  49044  linccl  49045  lincsum  49060  lincscmcl  49063  lcoss  49067  lincext1  49085  el0ldep  49097  lincresunit1  49108  lincresunit3  49112  lmod1zr  49124  fdivmptf  49172  refdivmptf  49173  1arymaptf  49272  aacllem  50430  amgmwlem  50431