Theorem fmpttd 7062

Description: Version of fmptd 7061 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 7061	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ↦ cmpt 5180  ⟶wf 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  fmpt3d  7063  fliftrel  7256  fsetfocdm  8802  pw2f1olem  9013  mapxpen  9075  fsuppssov1  9291  fsuppmptif  9306  wdom2d  9489  cantnflem1d  9601  cantnflem1  9602  ac5num  9950  acni2  9960  infpwfien  9976  fin23lem39  10264  fin1a2lem12  10325  canthp1lem2  10568  wuncval2  10662  gruf  10726  monoord2  13960  seqf1o  13970  ccatcl  14501  swrdcl  14573  swrdwrdsymb  14590  revcl  14688  revlen  14689  ello1mpt  15448  lo1o12  15460  lo1eq  15495  rlimeq  15496  climmpt2  15500  climrecl  15510  climge0  15511  o1compt  15514  rlimcn1b  15516  rlimdiv  15573  isercoll2  15596  caurcvg2  15605  fsumf1o  15650  sumss  15651  fsumss  15652  fsumcl2lem  15658  fsumadd  15667  isumclim3  15686  isummulc2  15689  fsummulc2  15711  fsumrelem  15734  climfsum  15747  isumshft  15766  divcnv  15780  prodfdiv  15823  fprodf1o  15873  prodss  15874  fprodss  15875  fprodser  15876  fprodcl2lem  15877  fprodmul  15887  fproddiv  15888  fprodn0  15906  iprodclim3  15927  fprodefsum  16022  iserodd  16767  prmreclem2  16849  vdwapf  16904  vdwlem4  16916  ramcl  16961  prmodvdslcmf  16979  prdsplusg  17382  prdsmulr  17383  prdsvsca  17384  mrcflem  17533  mreacs  17585  acsfn  17586  hofcllem  18185  hofcl  18186  yonedalem3a  18201  yonedalem4c  18204  yonedainv  18208  prdspjmhm  18758  pwsco1mhm  18761  pwsco2mhm  18762  gsumz  18765  gsumwspan  18775  odf1o1  19505  odf1o2  19506  sylow2blem1  19553  mulgmhm  19760  mulgghm  19761  iscyggen2  19814  cyggenod  19817  iscyg3  19819  gsumzsplit  19860  gsumsplit2  19862  gsumconst  19867  gsummptshft  19869  gsummhm2  19872  gsummptmhm  19873  gsummptf1o  19896  gsum2dlem1  19903  gsum2dlem2  19904  gsum2d  19905  prdsgsum  19914  dprdfeq0  19957  dprdlub  19961  dprdz  19965  dprd2dlem1  19976  dprd2da  19977  srglmhm  20160  srgrmhm  20161  ringlghm  20251  ringrghm  20252  gsumdixp  20258  pwspjmhmmgpd  20267  pwsgprod  20269  lmodvsghm  20878  gsumfsum  21393  regsumfsum  21394  expmhm  21395  expghm  21434  evpmodpmf1o  21555  frlmgsum  21731  frlmsplit2  21732  frlmphl  21740  uvcff  21750  uvcresum  21752  snifpsrbag  21880  psrass1lem  21892  rhmpsrlem1  21900  rhmpsrlem2  21901  psrmulcllem  21905  psrlidm  21921  psrridm  21922  psrcom  21927  resspsrmul  21935  mvrf  21944  mplmon  21994  mplmonmul  21995  mplcoe1  21996  mplcoe5lem  21998  mplcoe5  21999  mplbas2  22001  psrbagsn  22022  evlslem4  22035  evlslem2  22038  evlslem3  22039  evlslem6  22040  evlslem1  22041  evlsval2  22046  evlsval3  22048  evlsvvvallem  22050  evlsvvval  22052  psdcl  22108  psdmplcl  22109  psdmul  22113  psropprmul  22182  coe1mul2  22215  coe1tmmul2  22222  coe1tmmul  22223  ply1coe  22246  gsumsmonply1  22255  gsummoncoe1  22256  mamulid  22389  mamurid  22390  mdetunilem9  22568  mdetuni0  22569  mdetmul  22571  smadiadetlem3lem1  22614  m2cpmfo  22704  pmatcollpw1  22724  pmatcollpw3lem  22731  pmatcollpw3fi1lem2  22735  pm2mpcl  22745  mply1topmatcl  22753  mp2pm2mplem2  22755  mp2pm2mp  22759  pm2mpmhmlem2  22767  cayhamlem4  22836  pptbas  22956  tgrest  23107  resttopon  23109  rest0  23117  restfpw  23127  ordtbaslem  23136  ordtuni  23138  ordtrest  23150  cnpfval  23182  pnrmopn  23291  cncmp  23340  discmp  23346  1stcfb  23393  2ndcomap  23406  dis2ndc  23408  comppfsc  23480  kgencmp  23493  ptpjpre1  23519  ptpjcn  23559  ptcldmpt  23562  ptclsg  23563  dfac14  23566  xkoccn  23567  txcnp  23568  ptcnp  23570  uptx  23573  ptcn  23575  ptrescn  23587  xkoptsub  23602  xkoco1cn  23605  xkoco2cn  23606  cnmpt11  23611  pt1hmeo  23754  fbasrn  23832  trfilss  23837  trfg  23839  rnelfmlem  23900  flfcnp2  23955  fclscmpi  23977  alexsublem  23992  ptcmplem3  24002  symgtgp  24054  subgntr  24055  opnsubg  24056  clsnsg  24058  tgpconncomp  24061  eltsms  24081  haustsms  24084  tsmscls  24086  tsms0  24090  tsmsmhm  24094  tgptsmscls  24098  tsmssplit  24100  tsmsxplem1  24101  tsmsxplem2  24102  prdsdsf  24315  prdsxmetlem  24316  imasdsf1olem  24321  prdsbl  24439  stdbdxmet  24463  met1stc  24469  xrge0gsumle  24782  xrge0tsms  24783  cncfmpt2ss  24869  cnmptre  24881  evth  24918  evth2  24919  tcphcph  25197  rrxmval  25365  minveclem1  25384  minveclem3b  25388  iunmbl  25514  uniioombllem3  25546  ismbfcn2  25599  mbfeqalem1  25602  mbfeqalem2  25603  mbfss  25607  mbfmulc2re  25609  mbfneg  25611  mbfpos  25612  mbfposr  25613  mbfposb  25614  mbfadd  25622  mbfmulc2  25624  mbfsup  25625  mbfinf  25626  mbflimsup  25627  mbflimlem  25628  mbflim  25629  itg1climres  25675  mbfi1fseqlem3  25678  mbfi1fseqlem4  25679  mbfi1flimlem  25683  mbfi1flim  25684  mbfmullem2  25685  mbfmul  25687  itg2const2  25702  itg2seq  25703  itg2monolem1  25711  itg2monolem2  25712  itg2monolem3  25713  itg2mono  25714  itg2gt0  25721  itg2cnlem1  25722  itg2cnlem2  25723  itg2cn  25724  iblss  25766  itgitg1  25770  itgle  25771  itgeqa  25775  itgss3  25776  ibladdlem  25781  itgaddlem1  25784  iblabslem  25789  iblabs  25790  iblabsr  25791  iblmulc2  25792  itgmulc2lem1  25793  bddmulibl  25800  bddiblnc  25803  itggt0  25805  itgcn  25806  ellimc2  25838  limcmpt  25844  limcres  25847  limccnp  25852  limccnp2  25853  limcco  25854  perfdvf  25864  dvcnp2  25881  dvcnp2OLD  25882  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcjbr  25913  dvexp  25917  dvrec  25919  dvmptres3  25920  dvmptadd  25924  dvmptmul  25925  dvmptres2  25926  dvmptcmul  25928  dvmptcj  25932  dvmptntr  25935  dvmptco  25936  dvcnvlem  25940  dvef  25944  dvferm1  25949  dvferm2  25951  rolle  25954  dvlipcn  25959  dvle  25972  dvivth  25975  lhop1lem  25978  lhop1  25979  lhop2  25980  lhop  25981  dvfsumle  25986  dvfsumleOLD  25987  dvfsumge  25988  dvmptrecl  25990  dvfsumlem2  25993  dvfsumlem2OLD  25994  itgsubstlem  26015  itgpowd  26017  tdeglem4  26025  coe1mul3  26064  elply2  26161  plyf  26163  elplyd  26167  plypf1  26177  coeeq2  26207  coemullem  26215  coe1termlem  26223  dvply2g  26252  dvply2gOLD  26253  elqaalem2  26288  taylfvallem  26325  taylf  26328  tayl0  26329  taylpfval  26332  taylthlem1  26341  taylthlem2  26342  taylthlem2OLD  26343  ulmcau  26364  ulmss  26366  ulmdvlem3  26371  mtest  26373  mtestbdd  26374  itgulm2  26378  dvradcnv  26390  pserulm  26391  pserdvlem2  26398  abelthlem9  26410  pige3ALT  26489  logtayl  26629  logccv  26632  loglesqrt  26731  leibpi  26912  rlimcnp  26935  rlimcnp2  26936  xrlimcnp  26938  efrlim  26939  efrlimOLD  26940  dfef2  26941  o1cxp  26945  cxp2lim  26947  amgmlem  26960  lgamgulmlem2  27000  lgamgulmlem6  27004  lgamcvg2  27025  regamcl  27031  relgamcl  27032  basellem2  27052  basellem3  27053  sqff1o  27152  fsumvma  27184  dchrelbasd  27210  lgseisenlem3  27348  lgseisenlem4  27349  chpo1ub  27451  dchrisum0lem2a  27488  logsqvma2  27514  pnt2  27584  pnt  27585  incistruhgr  29135  minvecolem1  30932  hoaddcl  31816  homulcl  31817  cofmpt2  32694  mptiffisupp  32753  fpwrelmap  32793  gsummpt2d  33113  gsummptfsres  33118  gsummptf1od  33119  gsummptfsf1o  33124  gsumfs2d  33125  gsumzrsum  33129  gsummulsubdishift2  33133  gsummulsubdishift1s  33134  gsummulsubdishift2s  33135  xrge0tsmsd  33136  gsumwrd2dccat  33141  gsumvsca1  33289  gsumvsca2  33290  elrgspnlem1  33305  elrgspnlem2  33306  elrgspnlem3  33307  elrgspnlem4  33308  elrgspn  33309  elrgspnsubrunlem2  33311  elrspunidl  33490  elrspunsn  33491  ressply1evls1  33627  evl1deg2  33639  deg1prod  33645  extvfvcl  33682  evlextv  33688  mplvrpmga  33691  vietadeg1  33715  fedgmullem1  33767  fedgmullem2  33768  evls1fldgencl  33808  fldextrspunlsplem  33811  fldextrspunlsp  33812  extdgfialglem2  33831  ordtrestNEW  34059  esumf1o  34188  esumadd  34195  esumcst  34201  esumpfinval  34213  esumpcvgval  34216  esumcvg  34224  esumsup  34227  measinb  34359  measdivcst  34362  sitgclg  34480  dstfrvclim1  34616  gsumncl  34678  gsumnunsn  34679  fdvneggt  34738  fdvnegge  34740  itgexpif  34744  logdivsqrle  34788  indispconn  35409  cvxpconn  35417  cvmsss2  35449  cvmliftlem6  35465  cvmliftlem8  35467  mrsubcv  35685  mrsubff  35687  mrsubrn  35688  mrsubccat  35693  elmrsubrn  35695  msubrn  35704  msubff  35705  divcnvlin  35908  faclimlem2  35919  faclim  35921  faclim2  35923  knoppcnlem5  36672  knoppcnlem8  36675  knoppcnlem10  36677  knoppcnlem11  36678  curf  37770  finixpnum  37777  matunitlindflem1  37788  matunitlindflem2  37789  ptrest  37791  poimirlem17  37809  poimirlem20  37812  poimirlem24  37816  poimirlem30  37822  broucube  37826  mblfinlem2  37830  volsupnfl  37837  mbfposadd  37839  itg2addnclem2  37844  itg2gt0cn  37847  ibladdnclem  37848  itgaddnclem1  37850  itgaddnc  37852  iblabsnclem  37855  iblabsnc  37856  iblmulc2nc  37857  itgmulc2nclem1  37858  itgmulc2nclem2  37859  itgmulc2nc  37860  itgabsnc  37861  itggt0cn  37862  ftc1cnnc  37864  ftc1anclem1  37865  ftc1anclem2  37866  ftc1anclem3  37867  ftc1anclem4  37868  ftc1anclem5  37869  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anclem8  37872  ftc1anc  37873  areacirclem4  37883  upixp  37901  totbndbnd  37961  prdsbnd  37965  cntotbnd  37968  rrnequiv  38007  lsatlss  39293  tendoplcl  41078  tendoicl  41093  aks4d1p1p5  42366  aks4d1p9  42379  hashscontpow  42413  sticksstones10  42446  sticksstones17  42454  sticksstones18  42455  unitscyglem1  42486  redvmptabs  42651  fimgmcyc  42825  evlsbagval  42848  selvvvval  42864  evlselv  42866  fsuppind  42869  fsuppssind  42872  mhpind  42873  evlsmhpvvval  42874  mhphflem  42875  cmpfiiin  42975  mzpclall  43005  mzpindd  43024  fphpdo  43095  dnnumch3  43325  kelac1  43341  dfac21  43344  cantnfresb  43602  cantnf2  43603  tfsconcatrev  43626  rfovcnvf1od  44281  fsovfd  44289  fsovcnvlem  44290  clsk3nimkb  44317  mnringmulrcld  44505  expgrowth  44612  mptelpm  45456  mapss2  45485  monoord2xrv  45763  expcnfg  45873  clim1fr1  45883  sumnnodd  45912  limsupvaluz2  46018  supcnvlimsup  46020  climliminflimsupd  46081  liminfltlem  46084  cncfmptssg  46151  cncfcompt  46163  cxpcncf2  46179  dvsinax  46193  fperdvper  46199  dvcosax  46206  dvnmptdivc  46218  dvnprodlem2  46227  dvnprodlem3  46228  iblsplit  46246  itgcoscmulx  46249  itgiccshift  46260  itgperiod  46261  itgsbtaddcnst  46262  dirkerf  46377  dirkeritg  46382  hoidmvlelem1  46875  hoidmvlelem5  46879  ovnhoilem1  46881  ovnhoilem2  46882  ovnlecvr2  46890  ovncvr2  46891  hoidifhspf  46898  hspmbllem2  46907  opnvonmbllem2  46913  iccvonmbllem  46958  vonioolem1  46960  vonioolem2  46961  vonicclem1  46963  vonicclem2  46964  smfid  47032  cfsetsnfsetf  47340  funcringcsetcALTV2lem3  48574  funcringcsetclem3ALTV  48597  gsumlsscl  48662  ply1mulgsum  48672  lincfsuppcl  48695  linccl  48696  lincsum  48711  lincscmcl  48714  lcoss  48718  lincext1  48736  el0ldep  48748  lincresunit1  48759  lincresunit3  48763  lmod1zr  48775  fdivmptf  48823  refdivmptf  48824  1arymaptf  48923  aacllem  50082  amgmwlem  50083