Theorem fmpttd 6932

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110   ↦ cmpt 5135  ⟶wf 6376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-fun 6382  df-fn 6383  df-f 6384

This theorem is referenced by:  fmpt3d  6933  fliftrel  7117  pw2f1olem  8749  mapxpen  8812  fsuppmptif  9015  wdom2d  9196  cantnflem1d  9303  cantnflem1  9304  ac5num  9650  acni2  9660  infpwfien  9676  fin23lem39  9964  fin1a2lem12  10025  canthp1lem2  10267  wuncval2  10361  gruf  10425  monoord2  13607  seqf1o  13617  ccatcl  14129  swrdcl  14210  swrdwrdsymb  14227  revcl  14326  revlen  14327  ello1mpt  15082  lo1o12  15094  lo1eq  15129  rlimeq  15130  climmpt2  15134  climrecl  15144  climge0  15145  o1compt  15148  rlimcn1b  15150  rlimdiv  15209  isercoll2  15232  caurcvg2  15241  fsumf1o  15287  sumss  15288  fsumss  15289  fsumcl2lem  15295  fsumadd  15304  isumclim3  15323  isummulc2  15326  fsummulc2  15348  fsumrelem  15371  climfsum  15384  isumshft  15403  divcnv  15417  prodfdiv  15460  fprodf1o  15508  prodss  15509  fprodss  15510  fprodser  15511  fprodcl2lem  15512  fprodmul  15522  fproddiv  15523  fprodn0  15541  iprodclim3  15562  fprodefsum  15656  iserodd  16388  prmreclem2  16470  vdwapf  16525  vdwlem4  16537  ramcl  16582  prmodvdslcmf  16600  prdsplusg  16963  prdsmulr  16964  prdsvsca  16965  mrcflem  17109  mreacs  17161  acsfn  17162  hofcllem  17766  hofcl  17767  yonedalem3a  17782  yonedalem4c  17785  yonedainv  17789  prdspjmhm  18255  pwsco1mhm  18258  pwsco2mhm  18259  gsumz  18262  gsumwspan  18273  odf1o1  18961  odf1o2  18962  sylow2blem1  19009  mulgmhm  19213  mulgghm  19214  iscyggen2  19265  cyggenod  19268  iscyg3  19270  gsumzsplit  19312  gsumsplit2  19314  gsumconst  19319  gsummptshft  19321  gsummhm2  19324  gsummptmhm  19325  gsummptf1o  19348  gsum2dlem1  19355  gsum2dlem2  19356  gsum2d  19357  prdsgsum  19366  dprdfeq0  19409  dprdlub  19413  dprdz  19417  dprd2dlem1  19428  dprd2da  19429  srglmhm  19550  srgrmhm  19551  ringlghm  19622  ringrghm  19623  gsumdixp  19627  lmodvsghm  19960  gsumfsum  20430  regsumfsum  20431  expmhm  20432  expghm  20462  evpmodpmf1o  20558  frlmgsum  20734  frlmsplit2  20735  frlmphl  20743  uvcff  20753  uvcresum  20755  snifpsrbag  20881  psrass1lemOLD  20899  psrass1lem  20902  psrmulcllem  20912  psrlidm  20928  psrridm  20929  psrcom  20934  resspsrmul  20942  mvrf  20949  mplmon  20992  mplmonmul  20993  mplcoe1  20994  mplcoe5lem  20996  mplcoe5  20997  mplbas2  20999  psrbagsn  21021  evlslem4  21034  evlslem2  21039  evlslem3  21040  evlslem6  21041  evlslem1  21042  evlsval2  21047  psropprmul  21159  coe1mul2  21190  coe1tmmul2  21197  coe1tmmul  21198  ply1coe  21217  gsumsmonply1  21224  gsummoncoe1  21225  mamulid  21338  mamurid  21339  mdetunilem9  21517  mdetuni0  21518  mdetmul  21520  smadiadetlem3lem1  21563  m2cpmfo  21653  pmatcollpw1  21673  pmatcollpw3lem  21680  pmatcollpw3fi1lem2  21684  pm2mpcl  21694  mply1topmatcl  21702  mp2pm2mplem2  21704  mp2pm2mp  21708  pm2mpmhmlem2  21716  cayhamlem4  21785  pptbas  21905  tgrest  22056  resttopon  22058  rest0  22066  restfpw  22076  ordtbaslem  22085  ordtuni  22087  ordtrest  22099  cnpfval  22131  pnrmopn  22240  cncmp  22289  discmp  22295  1stcfb  22342  2ndcomap  22355  dis2ndc  22357  comppfsc  22429  kgencmp  22442  ptpjpre1  22468  ptpjcn  22508  ptcldmpt  22511  ptclsg  22512  dfac14  22515  xkoccn  22516  txcnp  22517  ptcnp  22519  uptx  22522  ptcn  22524  ptrescn  22536  xkoptsub  22551  xkoco1cn  22554  xkoco2cn  22555  cnmpt11  22560  pt1hmeo  22703  fbasrn  22781  trfilss  22786  trfg  22788  rnelfmlem  22849  flfcnp2  22904  fclscmpi  22926  alexsublem  22941  ptcmplem3  22951  symgtgp  23003  subgntr  23004  opnsubg  23005  clsnsg  23007  tgpconncomp  23010  eltsms  23030  haustsms  23033  tsmscls  23035  tsms0  23039  tsmsmhm  23043  tgptsmscls  23047  tsmssplit  23049  tsmsxplem1  23050  tsmsxplem2  23051  prdsdsf  23265  prdsxmetlem  23266  imasdsf1olem  23271  prdsbl  23389  stdbdxmet  23413  met1stc  23419  xrge0gsumle  23730  xrge0tsms  23731  cncfmpt2ss  23813  cnmptre  23824  evth  23856  evth2  23857  tcphcph  24134  rrxmval  24302  minveclem1  24321  minveclem3b  24325  iunmbl  24450  uniioombllem3  24482  ismbfcn2  24535  mbfeqalem1  24538  mbfeqalem2  24539  mbfss  24543  mbfmulc2re  24545  mbfneg  24547  mbfpos  24548  mbfposr  24549  mbfposb  24550  mbfadd  24558  mbfmulc2  24560  mbfsup  24561  mbfinf  24562  mbflimsup  24563  mbflimlem  24564  mbflim  24565  itg1climres  24612  mbfi1fseqlem3  24615  mbfi1fseqlem4  24616  mbfi1flimlem  24620  mbfi1flim  24621  mbfmullem2  24622  mbfmul  24624  itg2const2  24639  itg2seq  24640  itg2monolem1  24648  itg2monolem2  24649  itg2monolem3  24650  itg2mono  24651  itg2gt0  24658  itg2cnlem1  24659  itg2cnlem2  24660  itg2cn  24661  iblss  24702  itgitg1  24706  itgle  24707  itgeqa  24711  itgss3  24712  ibladdlem  24717  itgaddlem1  24720  iblabslem  24725  iblabs  24726  iblabsr  24727  iblmulc2  24728  itgmulc2lem1  24729  bddmulibl  24736  bddiblnc  24739  itggt0  24741  itgcn  24742  ellimc2  24774  limcmpt  24780  limcres  24783  limccnp  24788  limccnp2  24789  limcco  24790  perfdvf  24800  dvcnp2  24817  dvaddbr  24835  dvmulbr  24836  dvcjbr  24846  dvexp  24850  dvrec  24852  dvmptres3  24853  dvmptadd  24857  dvmptmul  24858  dvmptres2  24859  dvmptcmul  24861  dvmptcj  24865  dvmptntr  24868  dvmptco  24869  dvcnvlem  24873  dvef  24877  dvferm1  24882  dvferm2  24884  rolle  24887  dvlipcn  24891  dvle  24904  dvivth  24907  lhop1lem  24910  lhop1  24911  lhop2  24912  lhop  24913  dvfsumle  24918  dvfsumge  24919  dvmptrecl  24921  dvfsumlem2  24924  itgsubstlem  24945  itgpowd  24947  tdeglem4  24957  tdeglem4OLD  24958  coe1mul3  24997  elply2  25090  plyf  25092  elplyd  25096  plypf1  25106  coeeq2  25136  coemullem  25144  coe1termlem  25152  dvply2g  25178  elqaalem2  25213  taylfvallem  25250  taylf  25253  tayl0  25254  taylpfval  25257  taylthlem1  25265  taylthlem2  25266  ulmcau  25287  ulmss  25289  ulmdvlem3  25294  mtest  25296  mtestbdd  25297  itgulm2  25301  dvradcnv  25313  pserulm  25314  pserdvlem2  25320  abelthlem9  25332  pige3ALT  25409  logtayl  25548  logccv  25551  loglesqrt  25644  leibpi  25825  rlimcnp  25848  rlimcnp2  25849  xrlimcnp  25851  efrlim  25852  dfef2  25853  o1cxp  25857  cxp2lim  25859  amgmlem  25872  lgamgulmlem2  25912  lgamgulmlem6  25916  lgamcvg2  25937  regamcl  25943  relgamcl  25944  basellem2  25964  basellem3  25965  sqff1o  26064  fsumvma  26094  dchrelbasd  26120  lgseisenlem3  26258  lgseisenlem4  26259  chpo1ub  26361  dchrisum0lem2a  26398  logsqvma2  26424  pnt2  26494  pnt  26495  incistruhgr  27170  minvecolem1  28955  hoaddcl  29839  homulcl  29840  cofmpt2  30688  fpwrelmap  30788  gsummpt2d  31028  xrge0tsmsd  31036  gsumvsca1  31198  gsumvsca2  31199  elrspunidl  31320  fedgmullem1  31424  fedgmullem2  31425  ordtrestNEW  31585  esumf1o  31730  esumadd  31737  esumcst  31743  esumpfinval  31755  esumpcvgval  31758  esumcvg  31766  esumsup  31769  measinb  31901  measdivcst  31904  sitgclg  32021  dstfrvclim1  32156  gsumncl  32231  gsumnunsn  32232  fdvneggt  32292  fdvnegge  32294  itgexpif  32298  logdivsqrle  32342  indispconn  32909  cvxpconn  32917  cvmsss2  32949  cvmliftlem6  32965  cvmliftlem8  32967  mrsubcv  33185  mrsubff  33187  mrsubrn  33188  mrsubccat  33193  elmrsubrn  33195  msubrn  33204  msubff  33205  divcnvlin  33416  faclimlem2  33428  faclim  33430  faclim2  33432  knoppcnlem5  34414  knoppcnlem8  34417  knoppcnlem10  34419  knoppcnlem11  34420  curf  35492  finixpnum  35499  matunitlindflem1  35510  matunitlindflem2  35511  ptrest  35513  poimirlem17  35531  poimirlem20  35534  poimirlem24  35538  poimirlem30  35544  broucube  35548  mblfinlem2  35552  volsupnfl  35559  mbfposadd  35561  itg2addnclem2  35566  itg2gt0cn  35569  ibladdnclem  35570  itgaddnclem1  35572  itgaddnc  35574  iblabsnclem  35577  iblabsnc  35578  iblmulc2nc  35579  itgmulc2nclem1  35580  itgmulc2nclem2  35581  itgmulc2nc  35582  itgabsnc  35583  itggt0cn  35584  ftc1cnnc  35586  ftc1anclem1  35587  ftc1anclem2  35588  ftc1anclem3  35589  ftc1anclem4  35590  ftc1anclem5  35591  ftc1anclem6  35592  ftc1anclem7  35593  ftc1anclem8  35594  ftc1anc  35595  areacirclem4  35605  upixp  35624  totbndbnd  35684  prdsbnd  35688  cntotbnd  35691  rrnequiv  35730  lsatlss  36747  tendoplcl  38532  tendoicl  38547  aks4d1p1p5  39816  sticksstones10  39833  sticksstones17  39841  sticksstones18  39842  pwspjmhmmgpd  39979  pwsgprod  39981  evlsval3  39982  evlsbagval  39985  fsuppind  39989  fsuppssind  39992  mhpind  39993  mhphflem  39994  mhphf  39995  cmpfiiin  40222  mzpclall  40252  mzpindd  40271  fphpdo  40342  dnnumch3  40575  kelac1  40591  dfac21  40594  rfovcnvf1od  41289  fsovfd  41297  fsovcnvlem  41298  clsk3nimkb  41327  mnringmulrcld  41519  expgrowth  41626  mptelpm  42385  mapss2  42418  monoord2xrv  42699  expcnfg  42807  clim1fr1  42817  sumnnodd  42846  limsupvaluz2  42954  supcnvlimsup  42956  climliminflimsupd  43017  liminfltlem  43020  cncfmptssg  43087  cncfcompt  43099  cxpcncf2  43115  dvsinax  43129  fperdvper  43135  dvcosax  43142  dvnmptdivc  43154  dvnprodlem2  43163  dvnprodlem3  43164  iblsplit  43182  itgcoscmulx  43185  itgiccshift  43196  itgperiod  43197  itgsbtaddcnst  43198  dirkerf  43313  dirkeritg  43318  hoidmvlelem1  43808  hoidmvlelem5  43812  ovnhoilem1  43814  ovnhoilem2  43815  ovnlecvr2  43823  ovncvr2  43824  hoidifhspf  43831  hspmbllem2  43840  opnvonmbllem2  43846  iccvonmbllem  43891  vonioolem1  43893  vonioolem2  43894  vonicclem1  43896  vonicclem2  43897  smfid  43960  cfsetsnfsetf  44224  funcringcsetcALTV2lem3  45269  funcringcsetclem3ALTV  45292  gsumlsscl  45392  ply1mulgsum  45404  lincfsuppcl  45427  linccl  45428  lincsum  45443  lincscmcl  45446  lcoss  45450  lincext1  45468  el0ldep  45480  lincresunit1  45491  lincresunit3  45495  lmod1zr  45507  fdivmptf  45560  refdivmptf  45561  1arymaptf  45660  aacllem  46176  amgmwlem  46177