Theorem fmpttd 7115

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ↦ cmpt 5232  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-fun 6546  df-fn 6547  df-f 6548

This theorem is referenced by:  fmpt3d  7116  fliftrel  7305  pw2f1olem  9076  mapxpen  9143  fsuppmptif  9394  wdom2d  9575  cantnflem1d  9683  cantnflem1  9684  ac5num  10031  acni2  10041  infpwfien  10057  fin23lem39  10345  fin1a2lem12  10406  canthp1lem2  10648  wuncval2  10742  gruf  10806  monoord2  13999  seqf1o  14009  ccatcl  14524  swrdcl  14595  swrdwrdsymb  14612  revcl  14711  revlen  14712  ello1mpt  15465  lo1o12  15477  lo1eq  15512  rlimeq  15513  climmpt2  15517  climrecl  15527  climge0  15528  o1compt  15531  rlimcn1b  15533  rlimdiv  15592  isercoll2  15615  caurcvg2  15624  fsumf1o  15669  sumss  15670  fsumss  15671  fsumcl2lem  15677  fsumadd  15686  isumclim3  15705  isummulc2  15708  fsummulc2  15730  fsumrelem  15753  climfsum  15766  isumshft  15785  divcnv  15799  prodfdiv  15842  fprodf1o  15890  prodss  15891  fprodss  15892  fprodser  15893  fprodcl2lem  15894  fprodmul  15904  fproddiv  15905  fprodn0  15923  iprodclim3  15944  fprodefsum  16038  iserodd  16768  prmreclem2  16850  vdwapf  16905  vdwlem4  16917  ramcl  16962  prmodvdslcmf  16980  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  mrcflem  17550  mreacs  17602  acsfn  17603  hofcllem  18211  hofcl  18212  yonedalem3a  18227  yonedalem4c  18230  yonedainv  18234  prdspjmhm  18710  pwsco1mhm  18713  pwsco2mhm  18714  gsumz  18717  gsumwspan  18727  odf1o1  19440  odf1o2  19441  sylow2blem1  19488  mulgmhm  19695  mulgghm  19696  iscyggen2  19749  cyggenod  19752  iscyg3  19754  gsumzsplit  19795  gsumsplit2  19797  gsumconst  19802  gsummptshft  19804  gsummhm2  19807  gsummptmhm  19808  gsummptf1o  19831  gsum2dlem1  19838  gsum2dlem2  19839  gsum2d  19840  prdsgsum  19849  dprdfeq0  19892  dprdlub  19896  dprdz  19900  dprd2dlem1  19911  dprd2da  19912  srglmhm  20044  srgrmhm  20045  ringlghm  20124  ringrghm  20125  gsumdixp  20131  pwspjmhmmgpd  20141  lmodvsghm  20533  gsumfsum  21012  regsumfsum  21013  expmhm  21014  expghm  21045  evpmodpmf1o  21149  frlmgsum  21327  frlmsplit2  21328  frlmphl  21336  uvcff  21346  uvcresum  21348  snifpsrbag  21475  psrass1lemOLD  21493  psrass1lem  21496  psrmulcllem  21506  psrlidm  21523  psrridm  21524  psrcom  21529  resspsrmul  21537  mvrf  21544  mplmon  21590  mplmonmul  21591  mplcoe1  21592  mplcoe5lem  21594  mplcoe5  21595  mplbas2  21597  psrbagsn  21624  evlslem4  21637  evlslem2  21642  evlslem3  21643  evlslem6  21644  evlslem1  21645  evlsval2  21650  psropprmul  21760  coe1mul2  21791  coe1tmmul2  21798  coe1tmmul  21799  ply1coe  21820  gsumsmonply1  21827  gsummoncoe1  21828  mamulid  21943  mamurid  21944  mdetunilem9  22122  mdetuni0  22123  mdetmul  22125  smadiadetlem3lem1  22168  m2cpmfo  22258  pmatcollpw1  22278  pmatcollpw3lem  22285  pmatcollpw3fi1lem2  22289  pm2mpcl  22299  mply1topmatcl  22307  mp2pm2mplem2  22309  mp2pm2mp  22313  pm2mpmhmlem2  22321  cayhamlem4  22390  pptbas  22511  tgrest  22663  resttopon  22665  rest0  22673  restfpw  22683  ordtbaslem  22692  ordtuni  22694  ordtrest  22706  cnpfval  22738  pnrmopn  22847  cncmp  22896  discmp  22902  1stcfb  22949  2ndcomap  22962  dis2ndc  22964  comppfsc  23036  kgencmp  23049  ptpjpre1  23075  ptpjcn  23115  ptcldmpt  23118  ptclsg  23119  dfac14  23122  xkoccn  23123  txcnp  23124  ptcnp  23126  uptx  23129  ptcn  23131  ptrescn  23143  xkoptsub  23158  xkoco1cn  23161  xkoco2cn  23162  cnmpt11  23167  pt1hmeo  23310  fbasrn  23388  trfilss  23393  trfg  23395  rnelfmlem  23456  flfcnp2  23511  fclscmpi  23533  alexsublem  23548  ptcmplem3  23558  symgtgp  23610  subgntr  23611  opnsubg  23612  clsnsg  23614  tgpconncomp  23617  eltsms  23637  haustsms  23640  tsmscls  23642  tsms0  23646  tsmsmhm  23650  tgptsmscls  23654  tsmssplit  23656  tsmsxplem1  23657  tsmsxplem2  23658  prdsdsf  23873  prdsxmetlem  23874  imasdsf1olem  23879  prdsbl  24000  stdbdxmet  24024  met1stc  24030  xrge0gsumle  24349  xrge0tsms  24350  cncfmpt2ss  24432  cnmptre  24443  evth  24475  evth2  24476  tcphcph  24754  rrxmval  24922  minveclem1  24941  minveclem3b  24945  iunmbl  25070  uniioombllem3  25102  ismbfcn2  25155  mbfeqalem1  25158  mbfeqalem2  25159  mbfss  25163  mbfmulc2re  25165  mbfneg  25167  mbfpos  25168  mbfposr  25169  mbfposb  25170  mbfadd  25178  mbfmulc2  25180  mbfsup  25181  mbfinf  25182  mbflimsup  25183  mbflimlem  25184  mbflim  25185  itg1climres  25232  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1flimlem  25240  mbfi1flim  25241  mbfmullem2  25242  mbfmul  25244  itg2const2  25259  itg2seq  25260  itg2monolem1  25268  itg2monolem2  25269  itg2monolem3  25270  itg2mono  25271  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  itg2cn  25281  iblss  25322  itgitg1  25326  itgle  25327  itgeqa  25331  itgss3  25332  ibladdlem  25337  itgaddlem1  25340  iblabslem  25345  iblabs  25346  iblabsr  25347  iblmulc2  25348  itgmulc2lem1  25349  bddmulibl  25356  bddiblnc  25359  itggt0  25361  itgcn  25362  ellimc2  25394  limcmpt  25400  limcres  25403  limccnp  25408  limccnp2  25409  limcco  25410  perfdvf  25420  dvcnp2  25437  dvaddbr  25455  dvmulbr  25456  dvcjbr  25466  dvexp  25470  dvrec  25472  dvmptres3  25473  dvmptadd  25477  dvmptmul  25478  dvmptres2  25479  dvmptcmul  25481  dvmptcj  25485  dvmptntr  25488  dvmptco  25489  dvcnvlem  25493  dvef  25497  dvferm1  25502  dvferm2  25504  rolle  25507  dvlipcn  25511  dvle  25524  dvivth  25527  lhop1lem  25530  lhop1  25531  lhop2  25532  lhop  25533  dvfsumle  25538  dvfsumge  25539  dvmptrecl  25541  dvfsumlem2  25544  itgsubstlem  25565  itgpowd  25567  tdeglem4  25577  tdeglem4OLD  25578  coe1mul3  25617  elply2  25710  plyf  25712  elplyd  25716  plypf1  25726  coeeq2  25756  coemullem  25764  coe1termlem  25772  dvply2g  25798  elqaalem2  25833  taylfvallem  25870  taylf  25873  tayl0  25874  taylpfval  25877  taylthlem1  25885  taylthlem2  25886  ulmcau  25907  ulmss  25909  ulmdvlem3  25914  mtest  25916  mtestbdd  25917  itgulm2  25921  dvradcnv  25933  pserulm  25934  pserdvlem2  25940  abelthlem9  25952  pige3ALT  26029  logtayl  26168  logccv  26171  loglesqrt  26266  leibpi  26447  rlimcnp  26470  rlimcnp2  26471  xrlimcnp  26473  efrlim  26474  dfef2  26475  o1cxp  26479  cxp2lim  26481  amgmlem  26494  lgamgulmlem2  26534  lgamgulmlem6  26538  lgamcvg2  26559  regamcl  26565  relgamcl  26566  basellem2  26586  basellem3  26587  sqff1o  26686  fsumvma  26716  dchrelbasd  26742  lgseisenlem3  26880  lgseisenlem4  26881  chpo1ub  26983  dchrisum0lem2a  27020  logsqvma2  27046  pnt2  27116  pnt  27117  incistruhgr  28370  minvecolem1  30158  hoaddcl  31042  homulcl  31043  cofmpt2  31889  mptiffisupp  31946  fpwrelmap  31989  gsummpt2d  32232  xrge0tsmsd  32240  gsumvsca1  32402  gsumvsca2  32403  elrspunidl  32577  elrspunsn  32578  fedgmullem1  32745  fedgmullem2  32746  ordtrestNEW  32932  esumf1o  33079  esumadd  33086  esumcst  33092  esumpfinval  33104  esumpcvgval  33107  esumcvg  33115  esumsup  33118  measinb  33250  measdivcst  33253  sitgclg  33372  dstfrvclim1  33507  gsumncl  33582  gsumnunsn  33583  fdvneggt  33643  fdvnegge  33645  itgexpif  33649  logdivsqrle  33693  indispconn  34256  cvxpconn  34264  cvmsss2  34296  cvmliftlem6  34312  cvmliftlem8  34314  mrsubcv  34532  mrsubff  34534  mrsubrn  34535  mrsubccat  34540  elmrsubrn  34542  msubrn  34551  msubff  34552  divcnvlin  34733  faclimlem2  34745  faclim  34747  faclim2  34749  gg-dvcnp2  35205  gg-dvmulbr  35206  gg-dvfsumle  35213  gg-dvfsumlem2  35214  knoppcnlem5  35421  knoppcnlem8  35424  knoppcnlem10  35426  knoppcnlem11  35427  curf  36514  finixpnum  36521  matunitlindflem1  36532  matunitlindflem2  36533  ptrest  36535  poimirlem17  36553  poimirlem20  36556  poimirlem24  36560  poimirlem30  36566  broucube  36570  mblfinlem2  36574  volsupnfl  36581  mbfposadd  36583  itg2addnclem2  36588  itg2gt0cn  36591  ibladdnclem  36592  itgaddnclem1  36594  itgaddnc  36596  iblabsnclem  36599  iblabsnc  36600  iblmulc2nc  36601  itgmulc2nclem1  36602  itgmulc2nclem2  36603  itgmulc2nc  36604  itgabsnc  36605  itggt0cn  36606  ftc1cnnc  36608  ftc1anclem1  36609  ftc1anclem2  36610  ftc1anclem3  36611  ftc1anclem4  36612  ftc1anclem5  36613  ftc1anclem6  36614  ftc1anclem7  36615  ftc1anclem8  36616  ftc1anc  36617  areacirclem4  36627  upixp  36645  totbndbnd  36705  prdsbnd  36709  cntotbnd  36712  rrnequiv  36751  lsatlss  37914  tendoplcl  39700  tendoicl  39715  aks4d1p1p5  40988  aks4d1p9  41001  sticksstones10  41019  sticksstones17  41027  sticksstones18  41028  pwsgprod  41162  rhmmpllem1  41169  rhmmpllem2  41170  evlsval3  41179  evlsvvvallem  41181  evlsvvval  41183  evlsbagval  41186  selvvvval  41205  evlselv  41207  fsuppind  41210  fsuppssind  41213  mhpind  41214  evlsmhpvvval  41215  mhphflem  41216  cmpfiiin  41483  mzpclall  41513  mzpindd  41532  fphpdo  41603  dnnumch3  41837  kelac1  41853  dfac21  41856  cantnfresb  42122  cantnf2  42123  tfsconcatrev  42146  rfovcnvf1od  42803  fsovfd  42811  fsovcnvlem  42812  clsk3nimkb  42839  mnringmulrcld  43035  expgrowth  43142  mptelpm  43920  mapss2  43952  monoord2xrv  44242  expcnfg  44355  clim1fr1  44365  sumnnodd  44394  limsupvaluz2  44502  supcnvlimsup  44504  climliminflimsupd  44565  liminfltlem  44568  cncfmptssg  44635  cncfcompt  44647  cxpcncf2  44663  dvsinax  44677  fperdvper  44683  dvcosax  44690  dvnmptdivc  44702  dvnprodlem2  44711  dvnprodlem3  44712  iblsplit  44730  itgcoscmulx  44733  itgiccshift  44744  itgperiod  44745  itgsbtaddcnst  44746  dirkerf  44861  dirkeritg  44866  hoidmvlelem1  45359  hoidmvlelem5  45363  ovnhoilem1  45365  ovnhoilem2  45366  ovnlecvr2  45374  ovncvr2  45375  hoidifhspf  45382  hspmbllem2  45391  opnvonmbllem2  45397  iccvonmbllem  45442  vonioolem1  45444  vonioolem2  45445  vonicclem1  45447  vonicclem2  45448  smfid  45516  cfsetsnfsetf  45816  funcringcsetcALTV2lem3  46984  funcringcsetclem3ALTV  47007  gsumlsscl  47107  ply1mulgsum  47119  lincfsuppcl  47142  linccl  47143  lincsum  47158  lincscmcl  47161  lcoss  47165  lincext1  47183  el0ldep  47195  lincresunit1  47206  lincresunit3  47210  lmod1zr  47222  fdivmptf  47275  refdivmptf  47276  1arymaptf  47375  aacllem  47896  amgmwlem  47897