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  28339  minvecolem1  30127  hoaddcl  31011  homulcl  31012  cofmpt2  31858  mptiffisupp  31915  fpwrelmap  31958  gsummpt2d  32201  xrge0tsmsd  32209  gsumvsca1  32371  gsumvsca2  32372  elrspunidl  32546  elrspunsn  32547  fedgmullem1  32714  fedgmullem2  32715  ordtrestNEW  32901  esumf1o  33048  esumadd  33055  esumcst  33061  esumpfinval  33073  esumpcvgval  33076  esumcvg  33084  esumsup  33087  measinb  33219  measdivcst  33222  sitgclg  33341  dstfrvclim1  33476  gsumncl  33551  gsumnunsn  33552  fdvneggt  33612  fdvnegge  33614  itgexpif  33618  logdivsqrle  33662  indispconn  34225  cvxpconn  34233  cvmsss2  34265  cvmliftlem6  34281  cvmliftlem8  34283  mrsubcv  34501  mrsubff  34503  mrsubrn  34504  mrsubccat  34509  elmrsubrn  34511  msubrn  34520  msubff  34521  divcnvlin  34702  faclimlem2  34714  faclim  34716  faclim2  34718  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvfsumle  35182  gg-dvfsumlem2  35183  knoppcnlem5  35373  knoppcnlem8  35376  knoppcnlem10  35378  knoppcnlem11  35379  curf  36466  finixpnum  36473  matunitlindflem1  36484  matunitlindflem2  36485  ptrest  36487  poimirlem17  36505  poimirlem20  36508  poimirlem24  36512  poimirlem30  36518  broucube  36522  mblfinlem2  36526  volsupnfl  36533  mbfposadd  36535  itg2addnclem2  36540  itg2gt0cn  36543  ibladdnclem  36544  itgaddnclem1  36546  itgaddnc  36548  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  itgmulc2nclem1  36554  itgmulc2nclem2  36555  itgmulc2nc  36556  itgabsnc  36557  itggt0cn  36558  ftc1cnnc  36560  ftc1anclem1  36561  ftc1anclem2  36562  ftc1anclem3  36563  ftc1anclem4  36564  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  areacirclem4  36579  upixp  36597  totbndbnd  36657  prdsbnd  36661  cntotbnd  36664  rrnequiv  36703  lsatlss  37866  tendoplcl  39652  tendoicl  39667  aks4d1p1p5  40940  aks4d1p9  40953  sticksstones10  40971  sticksstones17  40979  sticksstones18  40980  pwsgprod  41114  rhmmpllem1  41121  rhmmpllem2  41122  evlsval3  41131  evlsvvvallem  41133  evlsvvval  41135  evlsbagval  41138  selvvvval  41157  evlselv  41159  fsuppind  41162  fsuppssind  41165  mhpind  41166  evlsmhpvvval  41167  mhphflem  41168  cmpfiiin  41435  mzpclall  41465  mzpindd  41484  fphpdo  41555  dnnumch3  41789  kelac1  41805  dfac21  41808  cantnfresb  42074  cantnf2  42075  tfsconcatrev  42098  rfovcnvf1od  42755  fsovfd  42763  fsovcnvlem  42764  clsk3nimkb  42791  mnringmulrcld  42987  expgrowth  43094  mptelpm  43872  mapss2  43904  monoord2xrv  44194  expcnfg  44307  clim1fr1  44317  sumnnodd  44346  limsupvaluz2  44454  supcnvlimsup  44456  climliminflimsupd  44517  liminfltlem  44520  cncfmptssg  44587  cncfcompt  44599  cxpcncf2  44615  dvsinax  44629  fperdvper  44635  dvcosax  44642  dvnmptdivc  44654  dvnprodlem2  44663  dvnprodlem3  44664  iblsplit  44682  itgcoscmulx  44685  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  dirkerf  44813  dirkeritg  44818  hoidmvlelem1  45311  hoidmvlelem5  45315  ovnhoilem1  45317  ovnhoilem2  45318  ovnlecvr2  45326  ovncvr2  45327  hoidifhspf  45334  hspmbllem2  45343  opnvonmbllem2  45349  iccvonmbllem  45394  vonioolem1  45396  vonioolem2  45397  vonicclem1  45399  vonicclem2  45400  smfid  45468  cfsetsnfsetf  45768  funcringcsetcALTV2lem3  46936  funcringcsetclem3ALTV  46959  gsumlsscl  47059  ply1mulgsum  47071  lincfsuppcl  47094  linccl  47095  lincsum  47110  lincscmcl  47113  lcoss  47117  lincext1  47135  el0ldep  47147  lincresunit1  47158  lincresunit3  47162  lmod1zr  47174  fdivmptf  47227  refdivmptf  47228  1arymaptf  47327  aacllem  47848  amgmwlem  47849