Theorem fmpttd 6700

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2050   ↦ cmpt 5004  ⟶wf 6181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5056  ax-nul 5063  ax-pr 5182

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3676  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-opab 4988  df-mpt 5005  df-id 5308  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-fv 6193

This theorem is referenced by:  fmpt3d  6701  fliftrel  6882  pw2f1olem  8415  mapxpen  8477  fsuppmptif  8656  wdom2d  8837  cantnflem1d  8943  cantnflem1  8944  ac5num  9254  acni2  9264  infpwfien  9280  fin23lem39  9568  fin1a2lem12  9629  canthp1lem2  9871  wuncval2  9965  gruf  10029  monoord2  13214  seqf1o  13224  ccatcl  13735  swrdcl  13806  swrdwrdsymb  13837  revcl  13978  revlen  13979  ello1mpt  14737  lo1o12  14749  lo1eq  14784  rlimeq  14785  climmpt2  14789  climrecl  14799  climge0  14800  o1compt  14803  rlimcn1b  14805  rlimdiv  14861  isercoll2  14884  caurcvg2  14893  fsumf1o  14938  sumss  14939  fsumss  14940  fsumcl2lem  14946  fsumadd  14954  isumclim3  14972  isummulc2  14975  fsummulc2  14997  fsumrelem  15020  climfsum  15033  isumshft  15052  divcnv  15066  prodfdiv  15110  fprodf1o  15158  prodss  15159  fprodss  15160  fprodser  15161  fprodcl2lem  15162  fprodmul  15172  fproddiv  15173  fprodn0  15191  iprodclim3  15212  fprodefsum  15306  iserodd  16026  prmreclem2  16107  vdwapf  16162  vdwlem4  16174  ramcl  16219  prmodvdslcmf  16237  prdsplusg  16585  prdsmulr  16586  prdsvsca  16587  mrcflem  16747  mreacs  16799  acsfn  16800  hofcllem  17378  hofcl  17379  yonedalem3a  17394  yonedalem4c  17397  yonedainv  17401  prdspjmhm  17847  pwsco1mhm  17850  pwsco2mhm  17851  gsumz  17854  gsumwspan  17864  psgnunilem5OLD  18396  odf1o1  18470  odf1o2  18471  sylow2blem1  18518  mulgmhm  18718  mulgghm  18719  iscyggen2  18768  cyggenod  18771  iscyg3  18773  gsumzsplit  18812  gsumsplit2  18814  gsumconst  18819  gsummptshft  18821  gsummhm2  18824  gsummptmhm  18825  gsummptf1o  18848  gsum2dlem1  18855  gsum2dlem2  18856  gsum2d  18857  prdsgsum  18863  dprdfeq0  18906  dprdlub  18910  dprdz  18914  dprd2dlem1  18925  dprd2da  18926  srglmhm  19020  srgrmhm  19021  ringlghm  19089  ringrghm  19090  gsumdixp  19094  lmodvsghm  19429  snifpsrbag  19872  psrass1lem  19883  psrmulcllem  19893  psrlidm  19909  psrridm  19910  psrcom  19915  resspsrmul  19923  mvrf  19930  mplmon  19969  mplmonmul  19970  mplcoe1  19971  mplcoe5lem  19973  mplcoe5  19974  mplbas2  19976  psrbagsn  20000  evlslem4  20013  evlslem2  20017  evlslem6  20018  evlslem3  20019  evlslem1  20020  evlsval2  20025  psropprmul  20121  coe1mul2  20152  coe1tmmul2  20159  coe1tmmul  20160  ply1coe  20179  gsumsmonply1  20186  gsummoncoe1  20187  gsumfsum  20326  regsumfsum  20327  expmhm  20328  expghm  20357  evpmodpmf1o  20454  frlmgsum  20630  frlmsplit2  20631  frlmphl  20639  uvcff  20649  uvcresum  20651  mamulid  20766  mamurid  20767  mdetunilem9  20945  mdetuni0  20946  mdetmul  20948  smadiadetlem3lem1  20991  m2cpmfo  21080  pmatcollpw1  21100  pmatcollpw3lem  21107  pmatcollpw3fi1lem2  21111  pm2mpcl  21121  mply1topmatcl  21129  mp2pm2mplem2  21131  mp2pm2mp  21135  pm2mpmhmlem2  21143  cayhamlem4  21212  pptbas  21332  tgrest  21483  resttopon  21485  rest0  21493  restfpw  21503  ordtbaslem  21512  ordtuni  21514  ordtrest  21526  cnpfval  21558  pnrmopn  21667  cncmp  21716  discmp  21722  1stcfb  21769  2ndcomap  21782  dis2ndc  21784  comppfsc  21856  kgencmp  21869  ptpjpre1  21895  ptpjcn  21935  ptcldmpt  21938  ptclsg  21939  dfac14  21942  xkoccn  21943  txcnp  21944  ptcnp  21946  uptx  21949  ptcn  21951  ptrescn  21963  xkoptsub  21978  xkoco1cn  21981  xkoco2cn  21982  cnmpt11  21987  pt1hmeo  22130  fbasrn  22208  trfilss  22213  trfg  22215  rnelfmlem  22276  flfcnp2  22331  fclscmpi  22353  alexsublem  22368  ptcmplem3  22378  symgtgp  22425  subgntr  22430  opnsubg  22431  clsnsg  22433  tgpconncomp  22436  eltsms  22456  haustsms  22459  tsmscls  22461  tsms0  22465  tsmsmhm  22469  tgptsmscls  22473  tsmssplit  22475  tsmsxplem1  22476  tsmsxplem2  22477  prdsdsf  22692  prdsxmetlem  22693  imasdsf1olem  22698  prdsbl  22816  stdbdxmet  22840  met1stc  22846  xrge0gsumle  23156  xrge0tsms  23157  cncfmpt2ss  23238  cnmptre  23246  evth  23278  evth2  23279  tcphcph  23555  rrxmval  23723  minveclem1  23742  minveclem3b  23746  iunmbl  23869  uniioombllem3  23901  ismbfcn2  23954  mbfeqalem1  23957  mbfeqalem2  23958  mbfss  23962  mbfmulc2re  23964  mbfneg  23966  mbfpos  23967  mbfposr  23968  mbfposb  23969  mbfadd  23977  mbfmulc2  23979  mbfsup  23980  mbfinf  23981  mbflimsup  23982  mbflimlem  23983  mbflim  23984  itg1climres  24030  mbfi1fseqlem3  24033  mbfi1fseqlem4  24034  mbfi1flimlem  24038  mbfi1flim  24039  mbfmullem2  24040  mbfmul  24042  itg2const2  24057  itg2seq  24058  itg2monolem1  24066  itg2monolem2  24067  itg2monolem3  24068  itg2mono  24069  itg2gt0  24076  itg2cnlem1  24077  itg2cnlem2  24078  itg2cn  24079  iblss  24120  itgitg1  24124  itgle  24125  itgeqa  24129  itgss3  24130  ibladdlem  24135  itgaddlem1  24138  iblabslem  24143  iblabs  24144  iblabsr  24145  iblmulc2  24146  itgmulc2lem1  24147  bddmulibl  24154  itggt0  24157  itgcn  24158  ellimc2  24190  limcmpt  24196  limcres  24199  limccnp  24204  limccnp2  24205  limcco  24206  perfdvf  24216  dvcnp2  24232  dvaddbr  24250  dvmulbr  24251  dvcjbr  24261  dvexp  24265  dvrec  24267  dvmptres3  24268  dvmptadd  24272  dvmptmul  24273  dvmptres2  24274  dvmptcmul  24276  dvmptcj  24280  dvmptntr  24283  dvmptco  24284  dvcnvlem  24288  dvef  24292  dvferm1  24297  dvferm2  24299  rolle  24302  dvlipcn  24306  dvle  24319  dvivth  24322  lhop1lem  24325  lhop1  24326  lhop2  24327  lhop  24328  dvfsumle  24333  dvfsumge  24334  dvmptrecl  24336  dvfsumlem2  24339  itgsubstlem  24360  tdeglem4  24369  coe1mul3  24408  elply2  24501  plyf  24503  elplyd  24507  plypf1  24517  coeeq2  24547  coemullem  24555  coe1termlem  24563  dvply2g  24589  elqaalem2  24624  taylfvallem  24661  taylf  24664  tayl0  24665  taylpfval  24668  taylthlem1  24676  taylthlem2  24677  ulmcau  24698  ulmss  24700  ulmdvlem3  24705  mtest  24707  mtestbdd  24708  itgulm2  24712  dvradcnv  24724  pserulm  24725  pserdvlem2  24731  abelthlem9  24743  pige3ALT  24820  logtayl  24956  logccv  24959  loglesqrt  25052  leibpi  25234  rlimcnp  25257  rlimcnp2  25258  xrlimcnp  25260  efrlim  25261  dfef2  25262  o1cxp  25266  cxp2lim  25268  amgmlem  25281  lgamgulmlem2  25321  lgamgulmlem6  25325  lgamcvg2  25346  regamcl  25352  relgamcl  25353  basellem2  25373  basellem3  25374  sqff1o  25473  fsumvma  25503  dchrelbasd  25529  lgseisenlem3  25667  lgseisenlem4  25668  chpo1ub  25770  dchrisum0lem2a  25807  logsqvma2  25833  pnt2  25903  pnt  25904  incistruhgr  26579  minvecolem1  28441  hoaddcl  29328  homulcl  29329  cofmpt2  30155  fpwrelmap  30242  gsummpt2d  30553  gsumvsca1  30554  gsumvsca2  30555  xrge0tsmsd  30559  fedgmullem1  30683  fedgmullem2  30684  ordtrestNEW  30837  esumf1o  30982  esumadd  30989  esumcst  30995  esumpfinval  31007  esumpcvgval  31010  esumcvg  31018  esumsup  31021  measinb  31154  measdivcst  31158  sitgclg  31274  dstfrvclim1  31410  gsumncl  31485  gsumnunsn  31486  fdvneggt  31548  fdvnegge  31550  itgexpif  31554  logdivsqrle  31598  indispconn  32095  cvxpconn  32103  cvmsss2  32135  cvmliftlem6  32151  cvmliftlem8  32153  mrsubcv  32306  mrsubff  32308  mrsubrn  32309  mrsubccat  32314  elmrsubrn  32316  msubrn  32325  msubff  32326  divcnvlin  32513  faclimlem2  32525  faclim  32527  faclim2  32529  knoppcnlem5  33385  knoppcnlem8  33388  knoppcnlem10  33390  knoppcnlem11  33391  curf  34340  finixpnum  34347  matunitlindflem1  34358  matunitlindflem2  34359  ptrest  34361  poimirlem17  34379  poimirlem20  34382  poimirlem24  34386  poimirlem30  34392  broucube  34396  mblfinlem2  34400  volsupnfl  34407  mbfposadd  34409  itg2addnclem2  34414  itg2gt0cn  34417  ibladdnclem  34418  itgaddnclem1  34420  itgaddnc  34422  iblabsnclem  34425  iblabsnc  34426  iblmulc2nc  34427  itgmulc2nclem1  34428  itgmulc2nclem2  34429  itgmulc2nc  34430  itgabsnc  34431  bddiblnc  34432  itggt0cn  34434  ftc1cnnc  34436  ftc1anclem1  34437  ftc1anclem2  34438  ftc1anclem3  34439  ftc1anclem4  34440  ftc1anclem5  34441  ftc1anclem6  34442  ftc1anclem7  34443  ftc1anclem8  34444  ftc1anc  34445  areacirclem4  34455  upixp  34475  totbndbnd  34538  prdsbnd  34542  cntotbnd  34545  rrnequiv  34584  lsatlss  35606  tendoplcl  37391  tendoicl  37406  cmpfiiin  38718  mzpclall  38748  mzpindd  38767  fphpdo  38839  dnnumch3  39072  kelac1  39088  dfac21  39091  itgpowd  39246  rfovcnvf1od  39742  fsovfd  39750  fsovcnvlem  39751  clsk3nimkb  39782  expgrowth  40112  mptelpm  40882  mapss2  40919  monoord2xrv  41216  expcnfg  41328  clim1fr1  41338  sumnnodd  41367  limsupvaluz2  41475  supcnvlimsup  41477  climliminflimsupd  41538  liminfltlem  41541  cncfmptssg  41608  cncfcompt  41621  cxpcncf2  41638  dvsinax  41652  fperdvper  41658  dvcosax  41666  dvnmptdivc  41678  dvnprodlem2  41687  dvnprodlem3  41688  iblsplit  41706  itgcoscmulx  41709  itgiccshift  41720  itgperiod  41721  itgsbtaddcnst  41722  dirkerf  41838  dirkeritg  41843  hoidmvlelem1  42333  hoidmvlelem5  42337  ovnhoilem1  42339  ovnhoilem2  42340  ovnlecvr2  42348  ovncvr2  42349  hoidifhspf  42356  hspmbllem2  42365  opnvonmbllem2  42371  iccvonmbllem  42416  vonioolem1  42418  vonioolem2  42419  vonicclem1  42421  vonicclem2  42422  smfid  42485  funcringcsetcALTV2lem3  43698  funcringcsetclem3ALTV  43721  gsumlsscl  43822  ply1mulgsum  43836  lincfsuppcl  43860  linccl  43861  lincsum  43876  lincscmcl  43879  lcoss  43883  lincext1  43901  el0ldep  43913  lincresunit1  43924  lincresunit3  43928  lmod1zr  43940  fdivmptf  43994  refdivmptf  43995  aacllem  44294  amgmwlem  44295