Theorem fmpttd 7090

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   ↦ cmpt 5180  ⟶wf 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-fun 6517  df-fn 6518  df-f 6519

This theorem is referenced by:  fmpt3d  7091  fliftrel  7286  fsetfocdm  8836  pw2f1olem  9047  mapxpen  9109  fsuppssov1  9325  fsuppmptif  9340  wdom2d  9523  cantnflem1d  9638  cantnflem1  9639  ac5num  9987  acni2  9997  infpwfien  10013  fin23lem39  10302  fin1a2lem12  10363  canthp1lem2  10606  wuncval2  10700  gruf  10764  monoord2  14041  seqf1o  14051  ccatcl  14582  swrdcl  14654  swrdwrdsymb  14671  revcl  14769  revlen  14770  ello1mpt  15529  lo1o12  15541  lo1eq  15576  rlimeq  15577  climmpt2  15581  climrecl  15591  climge0  15592  o1compt  15595  rlimcn1b  15597  rlimdiv  15654  isercoll2  15677  caurcvg2  15686  fsumf1o  15731  sumss  15732  fsumss  15733  fsumcl2lem  15739  fsumadd  15748  isumclim3  15767  isummulc2  15770  fsummulc2  15792  fsumrelem  15816  climfsum  15829  isumshft  15850  divcnv  15864  prodfdiv  15907  fprodf1o  15957  prodss  15958  fprodss  15959  fprodser  15960  fprodcl2lem  15961  fprodmul  15971  fproddiv  15972  fprodn0  15990  iprodclim3  16011  fprodefsum  16106  iserodd  16852  prmreclem2  16934  vdwapf  16989  vdwlem4  17001  ramcl  17046  prmodvdslcmf  17064  prdsplusg  17468  prdsmulr  17469  prdsvsca  17470  mrcflem  17619  mreacs  17671  acsfn  17672  hofcllem  18271  hofcl  18272  yonedalem3a  18287  yonedalem4c  18290  yonedainv  18294  prdspjmhm  18844  pwsco1mhm  18847  pwsco2mhm  18848  gsumz  18851  gsumwspan  18861  smndex1gbas  18917  odf1o1  19593  odf1o2  19594  sylow2blem1  19641  mulgmhm  19848  mulgghm  19849  iscyggen2  19902  cyggenod  19905  iscyg3  19907  gsumzsplit  19948  gsumsplit2  19950  gsumconst  19955  gsummptshft  19957  gsummhm2  19960  gsummptmhm  19961  gsummptf1o  19984  gsum2dlem1  19991  gsum2dlem2  19992  gsum2d  19993  prdsgsum  20002  dprdfeq0  20045  dprdlub  20049  dprdz  20053  dprd2dlem1  20064  dprd2da  20065  srglmhm  20248  srgrmhm  20249  ringlghm  20339  ringrghm  20340  gsumdixp  20344  pwspjmhmmgpd  20353  pwsgprod  20355  lmodvsghm  20968  gsumfsum  21464  regsumfsum  21465  expmhm  21466  expghm  21505  evpmodpmf1o  21626  frlmgsum  21802  frlmsplit2  21803  frlmphl  21811  uvcff  21821  uvcresum  21823  snifpsrbag  21950  psrass1lem  21963  rhmpsrlem1  21970  rhmpsrlem2  21971  psrmulcllem  21975  psrlidm  21991  psrridm  21992  psrcom  21997  resspsrmul  22005  mvrf  22014  mplmon  22066  mplmonmul  22067  mplcoe1  22068  mplcoe5lem  22070  mplcoe5  22071  mplbas2  22073  psrbagsn  22094  evlslem4  22107  evlslem2  22110  evlslem3  22111  evlslem6  22112  evlslem1  22113  evlsval2  22118  evlsval3  22120  evlsvvvallem  22122  evlsvvval  22124  selvvvval  22173  psdcl  22204  psdmplcl  22205  psdmul  22209  psropprmul  22277  coe1mul2  22310  coe1tmmul2  22317  coe1tmmul  22318  ply1coe  22339  gsumsmonply1  22348  gsummoncoe1  22349  mamulid  22479  mamurid  22480  mdetunilem9  22658  mdetuni0  22659  mdetmul  22661  smadiadetlem3lem1  22704  m2cpmfo  22794  pmatcollpw1  22814  pmatcollpw3lem  22821  pmatcollpw3fi1lem2  22825  pm2mpcl  22835  mply1topmatcl  22843  mp2pm2mplem2  22845  mp2pm2mp  22849  pm2mpmhmlem2  22857  cayhamlem4  22926  pptbas  23046  tgrest  23197  resttopon  23199  rest0  23207  restfpw  23217  ordtbaslem  23226  ordtuni  23228  ordtrest  23240  cnpfval  23272  pnrmopn  23381  cncmp  23430  discmp  23436  1stcfb  23483  2ndcomap  23496  dis2ndc  23498  comppfsc  23570  kgencmp  23583  ptpjpre1  23609  ptpjcn  23649  ptcldmpt  23652  ptclsg  23653  dfac14  23656  xkoccn  23657  txcnp  23658  ptcnp  23660  uptx  23663  ptcn  23665  ptrescn  23677  xkoptsub  23692  xkoco1cn  23695  xkoco2cn  23696  cnmpt11  23701  pt1hmeo  23844  fbasrn  23922  trfilss  23927  trfg  23929  rnelfmlem  23990  flfcnp2  24045  fclscmpi  24067  alexsublem  24082  ptcmplem3  24092  symgtgp  24144  subgntr  24145  opnsubg  24146  clsnsg  24148  tgpconncomp  24151  eltsms  24171  haustsms  24174  tsmscls  24176  tsms0  24180  tsmsmhm  24184  tgptsmscls  24188  tsmssplit  24190  tsmsxplem1  24191  tsmsxplem2  24192  prdsdsf  24405  prdsxmetlem  24406  imasdsf1olem  24411  prdsbl  24529  stdbdxmet  24553  met1stc  24559  xrge0gsumle  24872  xrge0tsms  24873  cncfmpt2ss  24956  cnmptre  24967  evth  24999  evth2  25000  tcphcph  25277  rrxmval  25445  minveclem1  25464  minveclem3b  25468  iunmbl  25593  uniioombllem3  25625  ismbfcn2  25678  mbfeqalem1  25681  mbfeqalem2  25682  mbfss  25686  mbfmulc2re  25688  mbfneg  25690  mbfpos  25691  mbfposr  25692  mbfposb  25693  mbfadd  25701  mbfmulc2  25703  mbfsup  25704  mbfinf  25705  mbflimsup  25706  mbflimlem  25707  mbflim  25708  itg1climres  25754  mbfi1fseqlem3  25757  mbfi1fseqlem4  25758  mbfi1flimlem  25762  mbfi1flim  25763  mbfmullem2  25764  mbfmul  25766  itg2const2  25781  itg2seq  25782  itg2monolem1  25790  itg2monolem2  25791  itg2monolem3  25792  itg2mono  25793  itg2gt0  25800  itg2cnlem1  25801  itg2cnlem2  25802  itg2cn  25803  iblss  25845  itgitg1  25849  itgle  25850  itgeqa  25854  itgss3  25855  ibladdlem  25860  itgaddlem1  25863  iblabslem  25868  iblabs  25869  iblabsr  25870  iblmulc2  25871  itgmulc2lem1  25872  bddmulibl  25879  bddiblnc  25882  itggt0  25884  itgcn  25885  ellimc2  25917  limcmpt  25923  limcres  25926  limccnp  25931  limccnp2  25932  limcco  25933  perfdvf  25943  dvcnp2  25960  dvaddbr  25978  dvmulbr  25979  dvcjbr  25989  dvexp  25993  dvrec  25995  dvmptres3  25996  dvmptadd  26000  dvmptmul  26001  dvmptres2  26002  dvmptcmul  26004  dvmptcj  26008  dvmptntr  26011  dvmptco  26012  dvcnvlem  26016  dvef  26020  dvferm1  26025  dvferm2  26027  rolle  26030  dvlipcn  26034  dvle  26047  dvivth  26050  lhop1lem  26053  lhop1  26054  lhop2  26055  lhop  26056  dvfsumle  26061  dvfsumge  26062  dvmptrecl  26064  dvfsumlem2  26067  itgsubstlem  26088  itgpowd  26090  tdeglem4  26098  coe1mul3  26137  elply2  26234  plyf  26236  elplyd  26240  plypf1  26250  coeeq2  26280  coemullem  26288  coe1termlem  26296  dvply2g  26324  elqaalem2  26359  taylfvallem  26396  taylf  26399  tayl0  26400  taylpfval  26403  taylthlem1  26411  taylthlem2  26412  ulmcau  26433  ulmss  26435  ulmdvlem3  26440  mtest  26442  mtestbdd  26443  itgulm2  26447  dvradcnv  26459  pserulm  26460  pserdvlem2  26466  abelthlem9  26478  pige3ALT  26560  logtayl  26700  logccv  26703  loglesqrt  26801  leibpi  26982  rlimcnp  27005  rlimcnp2  27006  xrlimcnp  27008  efrlim  27009  dfef2  27010  o1cxp  27014  cxp2lim  27016  amgmlem  27029  lgamgulmlem2  27069  lgamgulmlem6  27073  lgamcvg2  27094  regamcl  27100  relgamcl  27101  basellem2  27121  basellem3  27122  sqff1o  27221  fsumvma  27252  dchrelbasd  27278  lgseisenlem3  27416  lgseisenlem4  27417  chpo1ub  27519  dchrisum0lem2a  27556  logsqvma2  27582  pnt2  27652  pnt  27653  incistruhgr  29224  minvecolem1  31021  hoaddcl  31905  homulcl  31906  cofmpt2  32784  mptiffisupp  32843  fpwrelmap  32883  gsummpt2d  33188  gsummptfsres  33193  gsummptf1od  33194  gsummptfsf1o  33199  gsumfs2d  33200  gsumzrsum  33204  gsummulsubdishift2  33208  gsummulsubdishift1s  33209  gsummulsubdishift2s  33210  xrge0tsmsd  33212  gsumwrd2dccat  33217  gsumvsca1  33365  gsumvsca2  33366  elrgspnlem1  33382  elrgspnlem2  33383  elrgspnlem3  33384  elrgspnlem4  33385  elrgspn  33386  elrgspnsubrunlem2  33388  elrspunidl  33573  elrspunsn  33574  ressply1evls1  33720  evl1deg2  33732  deg1prod  33738  selvascl  33773  selvply1rhmlem1  33776  extvfvcl  33792  evlextv  33798  mplvrpmga  33801  psrgsum  33804  psrmon  33805  psrmonmul  33806  psrmonprod  33808  esplyfvaln  33830  vietadeg1  33834  fedgmullem1  33885  fedgmullem2  33886  evls1fldgencl  33926  fldextrspunlsplem  33929  fldextrspunlsp  33930  extdgfialglem2  33949  ordtrestNEW  34177  esumf1o  34306  esumadd  34313  esumcst  34319  esumpfinval  34331  esumpcvgval  34334  esumcvg  34342  esumsup  34345  measinb  34477  measdivcst  34480  sitgclg  34598  dstfrvclim1  34734  gsumncl  34796  gsumnunsn  34797  fdvneggt  34856  fdvnegge  34858  itgexpif  34862  logdivsqrle  34906  indispconn  35537  cvxpconn  35545  cvmsss2  35577  cvmliftlem6  35593  cvmliftlem8  35595  mrsubcv  35813  mrsubff  35815  mrsubrn  35816  mrsubccat  35821  elmrsubrn  35823  msubrn  35832  msubff  35833  divcnvlin  36036  faclimlem2  36047  faclim  36049  faclim2  36051  knoppcnlem5  36888  knoppcnlem8  36891  knoppcnlem10  36893  knoppcnlem11  36894  curf  38050  finixpnum  38057  matunitlindflem1  38068  matunitlindflem2  38069  ptrest  38071  poimirlem17  38089  poimirlem20  38092  poimirlem24  38096  poimirlem30  38102  broucube  38106  mblfinlem2  38110  volsupnfl  38117  mbfposadd  38119  itg2addnclem2  38124  itg2gt0cn  38127  ibladdnclem  38128  itgaddnclem1  38130  itgaddnc  38132  iblabsnclem  38135  iblabsnc  38136  iblmulc2nc  38137  itgmulc2nclem1  38138  itgmulc2nclem2  38139  itgmulc2nc  38140  itgabsnc  38141  itggt0cn  38142  ftc1cnnc  38144  ftc1anclem1  38145  ftc1anclem2  38146  ftc1anclem3  38147  ftc1anclem4  38148  ftc1anclem5  38149  ftc1anclem6  38150  ftc1anclem7  38151  ftc1anclem8  38152  ftc1anc  38153  areacirclem4  38163  upixp  38181  totbndbnd  38241  prdsbnd  38245  cntotbnd  38248  rrnequiv  38287  lsatlss  39573  tendoplcl  41358  tendoicl  41373  aks4d1p1p5  42645  aks4d1p9  42658  hashscontpow  42692  sticksstones10  42725  sticksstones17  42733  sticksstones18  42734  unitscyglem1  42765  redvmptabs  42922  fimgmcyc  43105  evlsbagval  43121  evlselv  43124  fsuppind  43125  fsuppssind  43128  mhpind  43129  evlsmhpvvval  43130  mhphflem  43131  cmpfiiin  43231  mzpclall  43261  mzpindd  43280  fphpdo  43347  dnnumch3  43577  kelac1  43593  dfac21  43596  cantnfresb  43854  cantnf2  43855  tfsconcatrev  43878  rfovcnvf1od  44533  fsovfd  44541  fsovcnvlem  44542  clsk3nimkb  44569  mnringmulrcld  44757  expgrowth  44864  mptelpm  45707  mapss2  45735  monoord2xrv  46010  expcnfg  46120  clim1fr1  46130  sumnnodd  46159  limsupvaluz2  46265  supcnvlimsup  46267  climliminflimsupd  46328  liminfltlem  46331  cncfmptssg  46398  cncfcompt  46410  cxpcncf2  46426  dvsinax  46440  fperdvper  46446  dvcosax  46453  dvnmptdivc  46465  dvnprodlem2  46474  dvnprodlem3  46475  iblsplit  46493  itgcoscmulx  46496  itgiccshift  46507  itgperiod  46508  itgsbtaddcnst  46509  dirkerf  46624  dirkeritg  46629  hoidmvlelem1  47122  hoidmvlelem5  47126  ovnhoilem1  47128  ovnhoilem2  47129  ovnlecvr2  47137  ovncvr2  47138  hoidifhspf  47145  hspmbllem2  47154  opnvonmbllem2  47160  iccvonmbllem  47205  vonioolem1  47207  vonioolem2  47208  vonicclem1  47210  vonicclem2  47211  smfid  47279  cfsetsnfsetf  47605  funcringcsetcALTV2lem3  48867  funcringcsetclem3ALTV  48890  gsumlsscl  48955  ply1mulgsum  48965  lincfsuppcl  48988  linccl  48989  lincsum  49004  lincscmcl  49007  lcoss  49011  lincext1  49029  el0ldep  49041  lincresunit1  49052  lincresunit3  49056  lmod1zr  49068  fdivmptf  49116  refdivmptf  49117  1arymaptf  49216  aacllem  50375  amgmwlem  50376