Theorem fmpttd 7059

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

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

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 5231  ax-pr 5368

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  fmpt3d  7060  fliftrel  7254  fsetfocdm  8799  pw2f1olem  9010  mapxpen  9072  fsuppssov1  9288  fsuppmptif  9303  wdom2d  9486  cantnflem1d  9598  cantnflem1  9599  ac5num  9947  acni2  9957  infpwfien  9973  fin23lem39  10261  fin1a2lem12  10322  canthp1lem2  10565  wuncval2  10659  gruf  10723  monoord2  13984  seqf1o  13994  ccatcl  14525  swrdcl  14597  swrdwrdsymb  14614  revcl  14712  revlen  14713  ello1mpt  15472  lo1o12  15484  lo1eq  15519  rlimeq  15520  climmpt2  15524  climrecl  15534  climge0  15535  o1compt  15538  rlimcn1b  15540  rlimdiv  15597  isercoll2  15620  caurcvg2  15629  fsumf1o  15674  sumss  15675  fsumss  15676  fsumcl2lem  15682  fsumadd  15691  isumclim3  15710  isummulc2  15713  fsummulc2  15735  fsumrelem  15759  climfsum  15772  isumshft  15793  divcnv  15807  prodfdiv  15850  fprodf1o  15900  prodss  15901  fprodss  15902  fprodser  15903  fprodcl2lem  15904  fprodmul  15914  fproddiv  15915  fprodn0  15933  iprodclim3  15954  fprodefsum  16049  iserodd  16795  prmreclem2  16877  vdwapf  16932  vdwlem4  16944  ramcl  16989  prmodvdslcmf  17007  prdsplusg  17410  prdsmulr  17411  prdsvsca  17412  mrcflem  17561  mreacs  17613  acsfn  17614  hofcllem  18213  hofcl  18214  yonedalem3a  18229  yonedalem4c  18232  yonedainv  18236  prdspjmhm  18786  pwsco1mhm  18789  pwsco2mhm  18790  gsumz  18793  gsumwspan  18803  smndex1gbas  18859  odf1o1  19536  odf1o2  19537  sylow2blem1  19584  mulgmhm  19791  mulgghm  19792  iscyggen2  19845  cyggenod  19848  iscyg3  19850  gsumzsplit  19891  gsumsplit2  19893  gsumconst  19898  gsummptshft  19900  gsummhm2  19903  gsummptmhm  19904  gsummptf1o  19927  gsum2dlem1  19934  gsum2dlem2  19935  gsum2d  19936  prdsgsum  19945  dprdfeq0  19988  dprdlub  19992  dprdz  19996  dprd2dlem1  20007  dprd2da  20008  srglmhm  20191  srgrmhm  20192  ringlghm  20282  ringrghm  20283  gsumdixp  20287  pwspjmhmmgpd  20296  pwsgprod  20298  lmodvsghm  20907  gsumfsum  21422  regsumfsum  21423  expmhm  21424  expghm  21463  evpmodpmf1o  21584  frlmgsum  21760  frlmsplit2  21761  frlmphl  21769  uvcff  21779  uvcresum  21781  snifpsrbag  21908  psrass1lem  21920  rhmpsrlem1  21928  rhmpsrlem2  21929  psrmulcllem  21933  psrlidm  21949  psrridm  21950  psrcom  21955  resspsrmul  21963  mvrf  21972  mplmon  22022  mplmonmul  22023  mplcoe1  22024  mplcoe5lem  22026  mplcoe5  22027  mplbas2  22029  psrbagsn  22050  evlslem4  22063  evlslem2  22066  evlslem3  22067  evlslem6  22068  evlslem1  22069  evlsval2  22074  evlsval3  22076  evlsvvvallem  22078  evlsvvval  22080  psdcl  22136  psdmplcl  22137  psdmul  22141  psropprmul  22210  coe1mul2  22243  coe1tmmul2  22250  coe1tmmul  22251  ply1coe  22272  gsumsmonply1  22281  gsummoncoe1  22282  mamulid  22415  mamurid  22416  mdetunilem9  22594  mdetuni0  22595  mdetmul  22597  smadiadetlem3lem1  22640  m2cpmfo  22730  pmatcollpw1  22750  pmatcollpw3lem  22757  pmatcollpw3fi1lem2  22761  pm2mpcl  22771  mply1topmatcl  22779  mp2pm2mplem2  22781  mp2pm2mp  22785  pm2mpmhmlem2  22793  cayhamlem4  22862  pptbas  22982  tgrest  23133  resttopon  23135  rest0  23143  restfpw  23153  ordtbaslem  23162  ordtuni  23164  ordtrest  23176  cnpfval  23208  pnrmopn  23317  cncmp  23366  discmp  23372  1stcfb  23419  2ndcomap  23432  dis2ndc  23434  comppfsc  23506  kgencmp  23519  ptpjpre1  23545  ptpjcn  23585  ptcldmpt  23588  ptclsg  23589  dfac14  23592  xkoccn  23593  txcnp  23594  ptcnp  23596  uptx  23599  ptcn  23601  ptrescn  23613  xkoptsub  23628  xkoco1cn  23631  xkoco2cn  23632  cnmpt11  23637  pt1hmeo  23780  fbasrn  23858  trfilss  23863  trfg  23865  rnelfmlem  23926  flfcnp2  23981  fclscmpi  24003  alexsublem  24018  ptcmplem3  24028  symgtgp  24080  subgntr  24081  opnsubg  24082  clsnsg  24084  tgpconncomp  24087  eltsms  24107  haustsms  24110  tsmscls  24112  tsms0  24116  tsmsmhm  24120  tgptsmscls  24124  tsmssplit  24126  tsmsxplem1  24127  tsmsxplem2  24128  prdsdsf  24341  prdsxmetlem  24342  imasdsf1olem  24347  prdsbl  24465  stdbdxmet  24489  met1stc  24495  xrge0gsumle  24808  xrge0tsms  24809  cncfmpt2ss  24892  cnmptre  24903  evth  24935  evth2  24936  tcphcph  25213  rrxmval  25381  minveclem1  25400  minveclem3b  25404  iunmbl  25529  uniioombllem3  25561  ismbfcn2  25614  mbfeqalem1  25617  mbfeqalem2  25618  mbfss  25622  mbfmulc2re  25624  mbfneg  25626  mbfpos  25627  mbfposr  25628  mbfposb  25629  mbfadd  25637  mbfmulc2  25639  mbfsup  25640  mbfinf  25641  mbflimsup  25642  mbflimlem  25643  mbflim  25644  itg1climres  25690  mbfi1fseqlem3  25693  mbfi1fseqlem4  25694  mbfi1flimlem  25698  mbfi1flim  25699  mbfmullem2  25700  mbfmul  25702  itg2const2  25717  itg2seq  25718  itg2monolem1  25726  itg2monolem2  25727  itg2monolem3  25728  itg2mono  25729  itg2gt0  25736  itg2cnlem1  25737  itg2cnlem2  25738  itg2cn  25739  iblss  25781  itgitg1  25785  itgle  25786  itgeqa  25790  itgss3  25791  ibladdlem  25796  itgaddlem1  25799  iblabslem  25804  iblabs  25805  iblabsr  25806  iblmulc2  25807  itgmulc2lem1  25808  bddmulibl  25815  bddiblnc  25818  itggt0  25820  itgcn  25821  ellimc2  25853  limcmpt  25859  limcres  25862  limccnp  25867  limccnp2  25868  limcco  25869  perfdvf  25879  dvcnp2  25896  dvaddbr  25914  dvmulbr  25915  dvcjbr  25925  dvexp  25929  dvrec  25931  dvmptres3  25932  dvmptadd  25936  dvmptmul  25937  dvmptres2  25938  dvmptcmul  25940  dvmptcj  25944  dvmptntr  25947  dvmptco  25948  dvcnvlem  25952  dvef  25956  dvferm1  25961  dvferm2  25963  rolle  25966  dvlipcn  25971  dvle  25984  dvivth  25987  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  dvfsumle  25998  dvfsumleOLD  25999  dvfsumge  26000  dvmptrecl  26002  dvfsumlem2  26005  dvfsumlem2OLD  26006  itgsubstlem  26027  itgpowd  26029  tdeglem4  26037  coe1mul3  26076  elply2  26173  plyf  26175  elplyd  26179  plypf1  26189  coeeq2  26219  coemullem  26227  coe1termlem  26235  dvply2g  26263  dvply2gOLD  26264  elqaalem2  26299  taylfvallem  26336  taylf  26339  tayl0  26340  taylpfval  26343  taylthlem1  26352  taylthlem2  26353  taylthlem2OLD  26354  ulmcau  26375  ulmss  26377  ulmdvlem3  26382  mtest  26384  mtestbdd  26385  itgulm2  26389  dvradcnv  26401  pserulm  26402  pserdvlem2  26409  abelthlem9  26421  pige3ALT  26500  logtayl  26640  logccv  26643  loglesqrt  26742  leibpi  26923  rlimcnp  26946  rlimcnp2  26947  xrlimcnp  26949  efrlim  26950  efrlimOLD  26951  dfef2  26952  o1cxp  26956  cxp2lim  26958  amgmlem  26971  lgamgulmlem2  27011  lgamgulmlem6  27015  lgamcvg2  27036  regamcl  27042  relgamcl  27043  basellem2  27063  basellem3  27064  sqff1o  27163  fsumvma  27195  dchrelbasd  27221  lgseisenlem3  27359  lgseisenlem4  27360  chpo1ub  27462  dchrisum0lem2a  27499  logsqvma2  27525  pnt2  27595  pnt  27596  incistruhgr  29167  minvecolem1  30965  hoaddcl  31849  homulcl  31850  cofmpt2  32727  mptiffisupp  32786  fpwrelmap  32826  gsummpt2d  33130  gsummptfsres  33135  gsummptf1od  33136  gsummptfsf1o  33141  gsumfs2d  33142  gsumzrsum  33146  gsummulsubdishift2  33150  gsummulsubdishift1s  33151  gsummulsubdishift2s  33152  xrge0tsmsd  33154  gsumwrd2dccat  33159  gsumvsca1  33307  gsumvsca2  33308  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  elrgspn  33327  elrgspnsubrunlem2  33329  elrspunidl  33508  elrspunsn  33509  ressply1evls1  33645  evl1deg2  33657  deg1prod  33663  extvfvcl  33700  evlextv  33706  mplvrpmga  33709  psrgsum  33712  psrmon  33713  psrmonmul  33714  psrmonprod  33716  esplyfvaln  33738  vietadeg1  33742  fedgmullem1  33794  fedgmullem2  33795  evls1fldgencl  33835  fldextrspunlsplem  33838  fldextrspunlsp  33839  extdgfialglem2  33858  ordtrestNEW  34086  esumf1o  34215  esumadd  34222  esumcst  34228  esumpfinval  34240  esumpcvgval  34243  esumcvg  34251  esumsup  34254  measinb  34386  measdivcst  34389  sitgclg  34507  dstfrvclim1  34643  gsumncl  34705  gsumnunsn  34706  fdvneggt  34765  fdvnegge  34767  itgexpif  34771  logdivsqrle  34815  indispconn  35437  cvxpconn  35445  cvmsss2  35477  cvmliftlem6  35493  cvmliftlem8  35495  mrsubcv  35713  mrsubff  35715  mrsubrn  35716  mrsubccat  35721  elmrsubrn  35723  msubrn  35732  msubff  35733  divcnvlin  35936  faclimlem2  35947  faclim  35949  faclim2  35951  knoppcnlem5  36770  knoppcnlem8  36773  knoppcnlem10  36775  knoppcnlem11  36776  curf  37930  finixpnum  37937  matunitlindflem1  37948  matunitlindflem2  37949  ptrest  37951  poimirlem17  37969  poimirlem20  37972  poimirlem24  37976  poimirlem30  37982  broucube  37986  mblfinlem2  37990  volsupnfl  37997  mbfposadd  37999  itg2addnclem2  38004  itg2gt0cn  38007  ibladdnclem  38008  itgaddnclem1  38010  itgaddnc  38012  iblabsnclem  38015  iblabsnc  38016  iblmulc2nc  38017  itgmulc2nclem1  38018  itgmulc2nclem2  38019  itgmulc2nc  38020  itgabsnc  38021  itggt0cn  38022  ftc1cnnc  38024  ftc1anclem1  38025  ftc1anclem2  38026  ftc1anclem3  38027  ftc1anclem4  38028  ftc1anclem5  38029  ftc1anclem6  38030  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033  areacirclem4  38043  upixp  38061  totbndbnd  38121  prdsbnd  38125  cntotbnd  38128  rrnequiv  38167  lsatlss  39453  tendoplcl  41238  tendoicl  41253  aks4d1p1p5  42525  aks4d1p9  42538  hashscontpow  42572  sticksstones10  42605  sticksstones17  42613  sticksstones18  42614  unitscyglem1  42645  redvmptabs  42803  fimgmcyc  42990  evlsbagval  43013  selvvvval  43029  evlselv  43031  fsuppind  43034  fsuppssind  43037  mhpind  43038  evlsmhpvvval  43039  mhphflem  43040  cmpfiiin  43140  mzpclall  43170  mzpindd  43189  fphpdo  43260  dnnumch3  43490  kelac1  43506  dfac21  43509  cantnfresb  43767  cantnf2  43768  tfsconcatrev  43791  rfovcnvf1od  44446  fsovfd  44454  fsovcnvlem  44455  clsk3nimkb  44482  mnringmulrcld  44670  expgrowth  44777  mptelpm  45621  mapss2  45649  monoord2xrv  45926  expcnfg  46036  clim1fr1  46046  sumnnodd  46075  limsupvaluz2  46181  supcnvlimsup  46183  climliminflimsupd  46244  liminfltlem  46247  cncfmptssg  46314  cncfcompt  46326  cxpcncf2  46342  dvsinax  46356  fperdvper  46362  dvcosax  46369  dvnmptdivc  46381  dvnprodlem2  46390  dvnprodlem3  46391  iblsplit  46409  itgcoscmulx  46412  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  dirkerf  46540  dirkeritg  46545  hoidmvlelem1  47038  hoidmvlelem5  47042  ovnhoilem1  47044  ovnhoilem2  47045  ovnlecvr2  47053  ovncvr2  47054  hoidifhspf  47061  hspmbllem2  47070  opnvonmbllem2  47076  iccvonmbllem  47121  vonioolem1  47123  vonioolem2  47124  vonicclem1  47126  vonicclem2  47127  smfid  47195  cfsetsnfsetf  47503  funcringcsetcALTV2lem3  48765  funcringcsetclem3ALTV  48788  gsumlsscl  48853  ply1mulgsum  48863  lincfsuppcl  48886  linccl  48887  lincsum  48902  lincscmcl  48905  lcoss  48909  lincext1  48927  el0ldep  48939  lincresunit1  48950  lincresunit3  48954  lmod1zr  48966  fdivmptf  49014  refdivmptf  49015  1arymaptf  49114  aacllem  50273  amgmwlem  50274