Theorem fmpttd 7063

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ↦ cmpt 5160  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-mpt 5161  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 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fmpt3d  7064  fliftrel  7259  fsetfocdm  8805  pw2f1olem  9016  mapxpen  9078  fsuppssov1  9294  fsuppmptif  9309  wdom2d  9492  cantnflem1d  9607  cantnflem1  9608  ac5num  9956  acni2  9966  infpwfien  9982  fin23lem39  10270  fin1a2lem12  10331  canthp1lem2  10574  wuncval2  10668  gruf  10732  monoord2  13993  seqf1o  14003  ccatcl  14534  swrdcl  14606  swrdwrdsymb  14623  revcl  14721  revlen  14722  ello1mpt  15481  lo1o12  15493  lo1eq  15528  rlimeq  15529  climmpt2  15533  climrecl  15543  climge0  15544  o1compt  15547  rlimcn1b  15549  rlimdiv  15606  isercoll2  15629  caurcvg2  15638  fsumf1o  15683  sumss  15684  fsumss  15685  fsumcl2lem  15691  fsumadd  15700  isumclim3  15719  isummulc2  15722  fsummulc2  15744  fsumrelem  15768  climfsum  15781  isumshft  15802  divcnv  15816  prodfdiv  15859  fprodf1o  15909  prodss  15910  fprodss  15911  fprodser  15912  fprodcl2lem  15913  fprodmul  15923  fproddiv  15924  fprodn0  15942  iprodclim3  15963  fprodefsum  16058  iserodd  16804  prmreclem2  16886  vdwapf  16941  vdwlem4  16953  ramcl  16998  prmodvdslcmf  17016  prdsplusg  17419  prdsmulr  17420  prdsvsca  17421  mrcflem  17570  mreacs  17622  acsfn  17623  hofcllem  18222  hofcl  18223  yonedalem3a  18238  yonedalem4c  18241  yonedainv  18245  prdspjmhm  18795  pwsco1mhm  18798  pwsco2mhm  18799  gsumz  18802  gsumwspan  18812  smndex1gbas  18868  odf1o1  19545  odf1o2  19546  sylow2blem1  19593  mulgmhm  19800  mulgghm  19801  iscyggen2  19854  cyggenod  19857  iscyg3  19859  gsumzsplit  19900  gsumsplit2  19902  gsumconst  19907  gsummptshft  19909  gsummhm2  19912  gsummptmhm  19913  gsummptf1o  19936  gsum2dlem1  19943  gsum2dlem2  19944  gsum2d  19945  prdsgsum  19954  dprdfeq0  19997  dprdlub  20001  dprdz  20005  dprd2dlem1  20016  dprd2da  20017  srglmhm  20200  srgrmhm  20201  ringlghm  20291  ringrghm  20292  gsumdixp  20296  pwspjmhmmgpd  20305  pwsgprod  20307  lmodvsghm  20920  gsumfsum  21416  regsumfsum  21417  expmhm  21418  expghm  21457  evpmodpmf1o  21578  frlmgsum  21754  frlmsplit2  21755  frlmphl  21763  uvcff  21773  uvcresum  21775  snifpsrbag  21902  psrass1lem  21915  rhmpsrlem1  21922  rhmpsrlem2  21923  psrmulcllem  21927  psrlidm  21943  psrridm  21944  psrcom  21949  resspsrmul  21957  mvrf  21966  mplmon  22018  mplmonmul  22019  mplcoe1  22020  mplcoe5lem  22022  mplcoe5  22023  mplbas2  22025  psrbagsn  22046  evlslem4  22059  evlslem2  22062  evlslem3  22063  evlslem6  22064  evlslem1  22065  evlsval2  22070  evlsval3  22072  evlsvvvallem  22074  evlsvvval  22076  selvvvval  22125  psdcl  22156  psdmplcl  22157  psdmul  22161  psropprmul  22229  coe1mul2  22262  coe1tmmul2  22269  coe1tmmul  22270  ply1coe  22291  gsumsmonply1  22300  gsummoncoe1  22301  mamulid  22431  mamurid  22432  mdetunilem9  22610  mdetuni0  22611  mdetmul  22613  smadiadetlem3lem1  22656  m2cpmfo  22746  pmatcollpw1  22766  pmatcollpw3lem  22773  pmatcollpw3fi1lem2  22777  pm2mpcl  22787  mply1topmatcl  22795  mp2pm2mplem2  22797  mp2pm2mp  22801  pm2mpmhmlem2  22809  cayhamlem4  22878  pptbas  22998  tgrest  23149  resttopon  23151  rest0  23159  restfpw  23169  ordtbaslem  23178  ordtuni  23180  ordtrest  23192  cnpfval  23224  pnrmopn  23333  cncmp  23382  discmp  23388  1stcfb  23435  2ndcomap  23448  dis2ndc  23450  comppfsc  23522  kgencmp  23535  ptpjpre1  23561  ptpjcn  23601  ptcldmpt  23604  ptclsg  23605  dfac14  23608  xkoccn  23609  txcnp  23610  ptcnp  23612  uptx  23615  ptcn  23617  ptrescn  23629  xkoptsub  23644  xkoco1cn  23647  xkoco2cn  23648  cnmpt11  23653  pt1hmeo  23796  fbasrn  23874  trfilss  23879  trfg  23881  rnelfmlem  23942  flfcnp2  23997  fclscmpi  24019  alexsublem  24034  ptcmplem3  24044  symgtgp  24096  subgntr  24097  opnsubg  24098  clsnsg  24100  tgpconncomp  24103  eltsms  24123  haustsms  24126  tsmscls  24128  tsms0  24132  tsmsmhm  24136  tgptsmscls  24140  tsmssplit  24142  tsmsxplem1  24143  tsmsxplem2  24144  prdsdsf  24357  prdsxmetlem  24358  imasdsf1olem  24363  prdsbl  24481  stdbdxmet  24505  met1stc  24511  xrge0gsumle  24824  xrge0tsms  24825  cncfmpt2ss  24908  cnmptre  24919  evth  24951  evth2  24952  tcphcph  25229  rrxmval  25397  minveclem1  25416  minveclem3b  25420  iunmbl  25545  uniioombllem3  25577  ismbfcn2  25630  mbfeqalem1  25633  mbfeqalem2  25634  mbfss  25638  mbfmulc2re  25640  mbfneg  25642  mbfpos  25643  mbfposr  25644  mbfposb  25645  mbfadd  25653  mbfmulc2  25655  mbfsup  25656  mbfinf  25657  mbflimsup  25658  mbflimlem  25659  mbflim  25660  itg1climres  25706  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  mbfi1flimlem  25714  mbfi1flim  25715  mbfmullem2  25716  mbfmul  25718  itg2const2  25733  itg2seq  25734  itg2monolem1  25742  itg2monolem2  25743  itg2monolem3  25744  itg2mono  25745  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  itg2cn  25755  iblss  25797  itgitg1  25801  itgle  25802  itgeqa  25806  itgss3  25807  ibladdlem  25812  itgaddlem1  25815  iblabslem  25820  iblabs  25821  iblabsr  25822  iblmulc2  25823  itgmulc2lem1  25824  bddmulibl  25831  bddiblnc  25834  itggt0  25836  itgcn  25837  ellimc2  25869  limcmpt  25875  limcres  25878  limccnp  25883  limccnp2  25884  limcco  25885  perfdvf  25895  dvcnp2  25912  dvaddbr  25930  dvmulbr  25931  dvcjbr  25941  dvexp  25945  dvrec  25947  dvmptres3  25948  dvmptadd  25952  dvmptmul  25953  dvmptres2  25954  dvmptcmul  25956  dvmptcj  25960  dvmptntr  25963  dvmptco  25964  dvcnvlem  25968  dvef  25972  dvferm1  25977  dvferm2  25979  rolle  25982  dvlipcn  25986  dvle  25999  dvivth  26002  lhop1lem  26005  lhop1  26006  lhop2  26007  lhop  26008  dvfsumle  26013  dvfsumge  26014  dvmptrecl  26016  dvfsumlem2  26019  itgsubstlem  26040  itgpowd  26042  tdeglem4  26050  coe1mul3  26089  elply2  26186  plyf  26188  elplyd  26192  plypf1  26202  coeeq2  26232  coemullem  26240  coe1termlem  26248  dvply2g  26276  elqaalem2  26311  taylfvallem  26348  taylf  26351  tayl0  26352  taylpfval  26355  taylthlem1  26363  taylthlem2  26364  ulmcau  26385  ulmss  26387  ulmdvlem3  26392  mtest  26394  mtestbdd  26395  itgulm2  26399  dvradcnv  26411  pserulm  26412  pserdvlem2  26418  abelthlem9  26430  pige3ALT  26509  logtayl  26649  logccv  26652  loglesqrt  26750  leibpi  26931  rlimcnp  26954  rlimcnp2  26955  xrlimcnp  26957  efrlim  26958  dfef2  26959  o1cxp  26963  cxp2lim  26965  amgmlem  26978  lgamgulmlem2  27018  lgamgulmlem6  27022  lgamcvg2  27043  regamcl  27049  relgamcl  27050  basellem2  27070  basellem3  27071  sqff1o  27170  fsumvma  27201  dchrelbasd  27227  lgseisenlem3  27365  lgseisenlem4  27366  chpo1ub  27468  dchrisum0lem2a  27505  logsqvma2  27531  pnt2  27601  pnt  27602  incistruhgr  29173  minvecolem1  30970  hoaddcl  31854  homulcl  31855  cofmpt2  32733  mptiffisupp  32792  fpwrelmap  32832  gsummpt2d  33137  gsummptfsres  33142  gsummptf1od  33143  gsummptfsf1o  33148  gsumfs2d  33149  gsumzrsum  33153  gsummulsubdishift2  33157  gsummulsubdishift1s  33158  gsummulsubdishift2s  33159  xrge0tsmsd  33161  gsumwrd2dccat  33166  gsumvsca1  33314  gsumvsca2  33315  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  elrgspn  33334  elrgspnsubrunlem2  33336  elrspunidl  33518  elrspunsn  33519  ressply1evls1  33655  evl1deg2  33667  deg1prod  33673  selvascl  33708  selvply1rhmlem1  33711  extvfvcl  33727  evlextv  33733  mplvrpmga  33736  psrgsum  33739  psrmon  33740  psrmonmul  33741  psrmonprod  33743  esplyfvaln  33765  vietadeg1  33769  fedgmullem1  33820  fedgmullem2  33821  evls1fldgencl  33861  fldextrspunlsplem  33864  fldextrspunlsp  33865  extdgfialglem2  33884  ordtrestNEW  34112  esumf1o  34241  esumadd  34248  esumcst  34254  esumpfinval  34266  esumpcvgval  34269  esumcvg  34277  esumsup  34280  measinb  34412  measdivcst  34415  sitgclg  34533  dstfrvclim1  34669  gsumncl  34731  gsumnunsn  34732  fdvneggt  34791  fdvnegge  34793  itgexpif  34797  logdivsqrle  34841  indispconn  35463  cvxpconn  35471  cvmsss2  35503  cvmliftlem6  35519  cvmliftlem8  35521  mrsubcv  35739  mrsubff  35741  mrsubrn  35742  mrsubccat  35747  elmrsubrn  35749  msubrn  35758  msubff  35759  divcnvlin  35962  faclimlem2  35973  faclim  35975  faclim2  35977  knoppcnlem5  36804  knoppcnlem8  36807  knoppcnlem10  36809  knoppcnlem11  36810  curf  37966  finixpnum  37973  matunitlindflem1  37984  matunitlindflem2  37985  ptrest  37987  poimirlem17  38005  poimirlem20  38008  poimirlem24  38012  poimirlem30  38018  broucube  38022  mblfinlem2  38026  volsupnfl  38033  mbfposadd  38035  itg2addnclem2  38040  itg2gt0cn  38043  ibladdnclem  38044  itgaddnclem1  38046  itgaddnc  38048  iblabsnclem  38051  iblabsnc  38052  iblmulc2nc  38053  itgmulc2nclem1  38054  itgmulc2nclem2  38055  itgmulc2nc  38056  itgabsnc  38057  itggt0cn  38058  ftc1cnnc  38060  ftc1anclem1  38061  ftc1anclem2  38062  ftc1anclem3  38063  ftc1anclem4  38064  ftc1anclem5  38065  ftc1anclem6  38066  ftc1anclem7  38067  ftc1anclem8  38068  ftc1anc  38069  areacirclem4  38079  upixp  38097  totbndbnd  38157  prdsbnd  38161  cntotbnd  38164  rrnequiv  38203  lsatlss  39489  tendoplcl  41274  tendoicl  41289  aks4d1p1p5  42561  aks4d1p9  42574  hashscontpow  42608  sticksstones10  42641  sticksstones17  42649  sticksstones18  42650  unitscyglem1  42681  redvmptabs  42838  fimgmcyc  43021  evlsbagval  43037  evlselv  43040  fsuppind  43041  fsuppssind  43044  mhpind  43045  evlsmhpvvval  43046  mhphflem  43047  cmpfiiin  43147  mzpclall  43177  mzpindd  43196  fphpdo  43263  dnnumch3  43493  kelac1  43509  dfac21  43512  cantnfresb  43770  cantnf2  43771  tfsconcatrev  43794  rfovcnvf1od  44449  fsovfd  44457  fsovcnvlem  44458  clsk3nimkb  44485  mnringmulrcld  44673  expgrowth  44780  mptelpm  45624  mapss2  45652  monoord2xrv  45927  expcnfg  46037  clim1fr1  46047  sumnnodd  46076  limsupvaluz2  46182  supcnvlimsup  46184  climliminflimsupd  46245  liminfltlem  46248  cncfmptssg  46315  cncfcompt  46327  cxpcncf2  46343  dvsinax  46357  fperdvper  46363  dvcosax  46370  dvnmptdivc  46382  dvnprodlem2  46391  dvnprodlem3  46392  iblsplit  46410  itgcoscmulx  46413  itgiccshift  46424  itgperiod  46425  itgsbtaddcnst  46426  dirkerf  46541  dirkeritg  46546  hoidmvlelem1  47039  hoidmvlelem5  47043  ovnhoilem1  47045  ovnhoilem2  47046  ovnlecvr2  47054  ovncvr2  47055  hoidifhspf  47062  hspmbllem2  47071  opnvonmbllem2  47077  iccvonmbllem  47122  vonioolem1  47124  vonioolem2  47125  vonicclem1  47127  vonicclem2  47128  smfid  47196  cfsetsnfsetf  47522  funcringcsetcALTV2lem3  48784  funcringcsetclem3ALTV  48807  gsumlsscl  48872  ply1mulgsum  48882  lincfsuppcl  48905  linccl  48906  lincsum  48921  lincscmcl  48924  lcoss  48928  lincext1  48946  el0ldep  48958  lincresunit1  48969  lincresunit3  48973  lmod1zr  48985  fdivmptf  49033  refdivmptf  49034  1arymaptf  49133  aacllem  50292  amgmwlem  50293