Theorem fmpttd 7149

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-fun 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  fmpt3d  7150  fliftrel  7344  fsetfocdm  8919  pw2f1olem  9142  mapxpen  9209  fsuppssov1  9453  fsuppmptif  9468  wdom2d  9649  cantnflem1d  9757  cantnflem1  9758  ac5num  10105  acni2  10115  infpwfien  10131  fin23lem39  10419  fin1a2lem12  10480  canthp1lem2  10722  wuncval2  10816  gruf  10880  monoord2  14084  seqf1o  14094  ccatcl  14622  swrdcl  14693  swrdwrdsymb  14710  revcl  14809  revlen  14810  ello1mpt  15567  lo1o12  15579  lo1eq  15614  rlimeq  15615  climmpt2  15619  climrecl  15629  climge0  15630  o1compt  15633  rlimcn1b  15635  rlimdiv  15694  isercoll2  15717  caurcvg2  15726  fsumf1o  15771  sumss  15772  fsumss  15773  fsumcl2lem  15779  fsumadd  15788  isumclim3  15807  isummulc2  15810  fsummulc2  15832  fsumrelem  15855  climfsum  15868  isumshft  15887  divcnv  15901  prodfdiv  15944  fprodf1o  15994  prodss  15995  fprodss  15996  fprodser  15997  fprodcl2lem  15998  fprodmul  16008  fproddiv  16009  fprodn0  16027  iprodclim3  16048  fprodefsum  16143  iserodd  16882  prmreclem2  16964  vdwapf  17019  vdwlem4  17031  ramcl  17076  prmodvdslcmf  17094  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  mrcflem  17664  mreacs  17716  acsfn  17717  hofcllem  18328  hofcl  18329  yonedalem3a  18344  yonedalem4c  18347  yonedainv  18351  prdspjmhm  18864  pwsco1mhm  18867  pwsco2mhm  18868  gsumz  18871  gsumwspan  18881  odf1o1  19614  odf1o2  19615  sylow2blem1  19662  mulgmhm  19869  mulgghm  19870  iscyggen2  19923  cyggenod  19926  iscyg3  19928  gsumzsplit  19969  gsumsplit2  19971  gsumconst  19976  gsummptshft  19978  gsummhm2  19981  gsummptmhm  19982  gsummptf1o  20005  gsum2dlem1  20012  gsum2dlem2  20013  gsum2d  20014  prdsgsum  20023  dprdfeq0  20066  dprdlub  20070  dprdz  20074  dprd2dlem1  20085  dprd2da  20086  srglmhm  20248  srgrmhm  20249  ringlghm  20335  ringrghm  20336  gsumdixp  20342  pwspjmhmmgpd  20351  lmodvsghm  20943  gsumfsum  21475  regsumfsum  21476  expmhm  21477  expghm  21509  evpmodpmf1o  21637  frlmgsum  21815  frlmsplit2  21816  frlmphl  21824  uvcff  21834  uvcresum  21836  snifpsrbag  21963  psrass1lem  21975  rhmpsrlem1  21983  rhmpsrlem2  21984  psrmulcllem  21988  psrlidm  22005  psrridm  22006  psrcom  22011  resspsrmul  22019  mvrf  22028  mplmon  22076  mplmonmul  22077  mplcoe1  22078  mplcoe5lem  22080  mplcoe5  22081  mplbas2  22083  psrbagsn  22110  evlslem4  22123  evlslem2  22126  evlslem3  22127  evlslem6  22128  evlslem1  22129  evlsval2  22134  psdcl  22188  psdmplcl  22189  psdmul  22193  psropprmul  22260  coe1mul2  22293  coe1tmmul2  22300  coe1tmmul  22301  ply1coe  22323  gsumsmonply1  22332  gsummoncoe1  22333  mamulid  22468  mamurid  22469  mdetunilem9  22647  mdetuni0  22648  mdetmul  22650  smadiadetlem3lem1  22693  m2cpmfo  22783  pmatcollpw1  22803  pmatcollpw3lem  22810  pmatcollpw3fi1lem2  22814  pm2mpcl  22824  mply1topmatcl  22832  mp2pm2mplem2  22834  mp2pm2mp  22838  pm2mpmhmlem2  22846  cayhamlem4  22915  pptbas  23036  tgrest  23188  resttopon  23190  rest0  23198  restfpw  23208  ordtbaslem  23217  ordtuni  23219  ordtrest  23231  cnpfval  23263  pnrmopn  23372  cncmp  23421  discmp  23427  1stcfb  23474  2ndcomap  23487  dis2ndc  23489  comppfsc  23561  kgencmp  23574  ptpjpre1  23600  ptpjcn  23640  ptcldmpt  23643  ptclsg  23644  dfac14  23647  xkoccn  23648  txcnp  23649  ptcnp  23651  uptx  23654  ptcn  23656  ptrescn  23668  xkoptsub  23683  xkoco1cn  23686  xkoco2cn  23687  cnmpt11  23692  pt1hmeo  23835  fbasrn  23913  trfilss  23918  trfg  23920  rnelfmlem  23981  flfcnp2  24036  fclscmpi  24058  alexsublem  24073  ptcmplem3  24083  symgtgp  24135  subgntr  24136  opnsubg  24137  clsnsg  24139  tgpconncomp  24142  eltsms  24162  haustsms  24165  tsmscls  24167  tsms0  24171  tsmsmhm  24175  tgptsmscls  24179  tsmssplit  24181  tsmsxplem1  24182  tsmsxplem2  24183  prdsdsf  24398  prdsxmetlem  24399  imasdsf1olem  24404  prdsbl  24525  stdbdxmet  24549  met1stc  24555  xrge0gsumle  24874  xrge0tsms  24875  cncfmpt2ss  24961  cnmptre  24973  evth  25010  evth2  25011  tcphcph  25290  rrxmval  25458  minveclem1  25477  minveclem3b  25481  iunmbl  25607  uniioombllem3  25639  ismbfcn2  25692  mbfeqalem1  25695  mbfeqalem2  25696  mbfss  25700  mbfmulc2re  25702  mbfneg  25704  mbfpos  25705  mbfposr  25706  mbfposb  25707  mbfadd  25715  mbfmulc2  25717  mbfsup  25718  mbfinf  25719  mbflimsup  25720  mbflimlem  25721  mbflim  25722  itg1climres  25769  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1flimlem  25777  mbfi1flim  25778  mbfmullem2  25779  mbfmul  25781  itg2const2  25796  itg2seq  25797  itg2monolem1  25805  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  itg2cn  25818  iblss  25860  itgitg1  25864  itgle  25865  itgeqa  25869  itgss3  25870  ibladdlem  25875  itgaddlem1  25878  iblabslem  25883  iblabs  25884  iblabsr  25885  iblmulc2  25886  itgmulc2lem1  25887  bddmulibl  25894  bddiblnc  25897  itggt0  25899  itgcn  25900  ellimc2  25932  limcmpt  25938  limcres  25941  limccnp  25946  limccnp2  25947  limcco  25948  perfdvf  25958  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcjbr  26007  dvexp  26011  dvrec  26013  dvmptres3  26014  dvmptadd  26018  dvmptmul  26019  dvmptres2  26020  dvmptcmul  26022  dvmptcj  26026  dvmptntr  26029  dvmptco  26030  dvcnvlem  26034  dvef  26038  dvferm1  26043  dvferm2  26045  rolle  26048  dvlipcn  26053  dvle  26066  dvivth  26069  lhop1lem  26072  lhop1  26073  lhop2  26074  lhop  26075  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvmptrecl  26084  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgsubstlem  26109  itgpowd  26111  tdeglem4  26119  coe1mul3  26158  elply2  26255  plyf  26257  elplyd  26261  plypf1  26271  coeeq2  26301  coemullem  26309  coe1termlem  26317  dvply2g  26344  dvply2gOLD  26345  elqaalem2  26380  taylfvallem  26417  taylf  26420  tayl0  26421  taylpfval  26424  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmcau  26456  ulmss  26458  ulmdvlem3  26463  mtest  26465  mtestbdd  26466  itgulm2  26470  dvradcnv  26482  pserulm  26483  pserdvlem2  26490  abelthlem9  26502  pige3ALT  26580  logtayl  26720  logccv  26723  loglesqrt  26822  leibpi  27003  rlimcnp  27026  rlimcnp2  27027  xrlimcnp  27029  efrlim  27030  efrlimOLD  27031  dfef2  27032  o1cxp  27036  cxp2lim  27038  amgmlem  27051  lgamgulmlem2  27091  lgamgulmlem6  27095  lgamcvg2  27116  regamcl  27122  relgamcl  27123  basellem2  27143  basellem3  27144  sqff1o  27243  fsumvma  27275  dchrelbasd  27301  lgseisenlem3  27439  lgseisenlem4  27440  chpo1ub  27542  dchrisum0lem2a  27579  logsqvma2  27605  pnt2  27675  pnt  27676  incistruhgr  29114  minvecolem1  30906  hoaddcl  31790  homulcl  31791  cofmpt2  32653  mptiffisupp  32705  fpwrelmap  32747  gsummpt2d  33032  xrge0tsmsd  33041  gsumvsca1  33205  gsumvsca2  33206  elrspunidl  33421  elrspunsn  33422  evl1deg2  33567  fedgmullem1  33642  fedgmullem2  33643  evls1fldgencl  33680  ordtrestNEW  33867  esumf1o  34014  esumadd  34021  esumcst  34027  esumpfinval  34039  esumpcvgval  34042  esumcvg  34050  esumsup  34053  measinb  34185  measdivcst  34188  sitgclg  34307  dstfrvclim1  34442  gsumncl  34517  gsumnunsn  34518  fdvneggt  34577  fdvnegge  34579  itgexpif  34583  logdivsqrle  34627  indispconn  35202  cvxpconn  35210  cvmsss2  35242  cvmliftlem6  35258  cvmliftlem8  35260  mrsubcv  35478  mrsubff  35480  mrsubrn  35481  mrsubccat  35486  elmrsubrn  35488  msubrn  35497  msubff  35498  divcnvlin  35695  faclimlem2  35706  faclim  35708  faclim2  35710  knoppcnlem5  36463  knoppcnlem8  36466  knoppcnlem10  36468  knoppcnlem11  36469  curf  37558  finixpnum  37565  matunitlindflem1  37576  matunitlindflem2  37577  ptrest  37579  poimirlem17  37597  poimirlem20  37600  poimirlem24  37604  poimirlem30  37610  broucube  37614  mblfinlem2  37618  volsupnfl  37625  mbfposadd  37627  itg2addnclem2  37632  itg2gt0cn  37635  ibladdnclem  37636  itgaddnclem1  37638  itgaddnc  37640  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  itgmulc2nclem1  37646  itgmulc2nclem2  37647  itgmulc2nc  37648  itgabsnc  37649  itggt0cn  37650  ftc1cnnc  37652  ftc1anclem1  37653  ftc1anclem2  37654  ftc1anclem3  37655  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  areacirclem4  37671  upixp  37689  totbndbnd  37749  prdsbnd  37753  cntotbnd  37756  rrnequiv  37795  lsatlss  38952  tendoplcl  40738  tendoicl  40753  aks4d1p1p5  42032  aks4d1p9  42045  hashscontpow  42079  sticksstones10  42112  sticksstones17  42120  sticksstones18  42121  unitscyglem1  42152  fimgmcyc  42489  pwsgprod  42499  evlsval3  42514  evlsvvvallem  42516  evlsvvval  42518  evlsbagval  42521  selvvvval  42540  evlselv  42542  fsuppind  42545  fsuppssind  42548  mhpind  42549  evlsmhpvvval  42550  mhphflem  42551  cmpfiiin  42653  mzpclall  42683  mzpindd  42702  fphpdo  42773  dnnumch3  43004  kelac1  43020  dfac21  43023  cantnfresb  43286  cantnf2  43287  tfsconcatrev  43310  rfovcnvf1od  43966  fsovfd  43974  fsovcnvlem  43975  clsk3nimkb  44002  mnringmulrcld  44197  expgrowth  44304  mptelpm  45083  mapss2  45112  monoord2xrv  45399  expcnfg  45512  clim1fr1  45522  sumnnodd  45551  limsupvaluz2  45659  supcnvlimsup  45661  climliminflimsupd  45722  liminfltlem  45725  cncfmptssg  45792  cncfcompt  45804  cxpcncf2  45820  dvsinax  45834  fperdvper  45840  dvcosax  45847  dvnmptdivc  45859  dvnprodlem2  45868  dvnprodlem3  45869  iblsplit  45887  itgcoscmulx  45890  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  dirkerf  46018  dirkeritg  46023  hoidmvlelem1  46516  hoidmvlelem5  46520  ovnhoilem1  46522  ovnhoilem2  46523  ovnlecvr2  46531  ovncvr2  46532  hoidifhspf  46539  hspmbllem2  46548  opnvonmbllem2  46554  iccvonmbllem  46599  vonioolem1  46601  vonioolem2  46602  vonicclem1  46604  vonicclem2  46605  smfid  46673  cfsetsnfsetf  46973  funcringcsetcALTV2lem3  48015  funcringcsetclem3ALTV  48038  gsumlsscl  48108  ply1mulgsum  48119  lincfsuppcl  48142  linccl  48143  lincsum  48158  lincscmcl  48161  lcoss  48165  lincext1  48183  el0ldep  48195  lincresunit1  48206  lincresunit3  48210  lmod1zr  48222  fdivmptf  48275  refdivmptf  48276  1arymaptf  48375  aacllem  48895  amgmwlem  48896