Theorem fmpttd 7110

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141   ↦ cmpt 5191  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  fmpt3d  7111  fliftrel  7306  fsetfocdm  8857  pw2f1olem  9068  mapxpen  9130  fsuppssov1  9343  fsuppmptif  9358  wdom2d  9541  cantnflem1d  9656  cantnflem1  9657  ac5num  10019  acni2  10029  infpwfien  10045  fin23lem39  10333  fin1a2lem12  10394  canthp1lem2  10637  wuncval2  10731  gruf  10795  monoord2  14069  seqf1o  14079  ccatcl  14611  swrdcl  14683  swrdwrdsymb  14700  revcl  14798  revlen  14799  ello1mpt  15572  lo1o12  15584  lo1eq  15619  rlimeq  15620  climmpt2  15624  climrecl  15634  climge0  15635  o1compt  15638  rlimcn1b  15640  rlimdiv  15697  isercoll2  15720  caurcvg2  15729  fsumf1o  15774  sumss  15775  fsumss  15776  fsumcl2lem  15782  fsumadd  15791  isumclim3  15810  isummulc2  15813  fsummulc2  15835  fsumrelem  15859  climfsum  15872  isumshft  15893  divcnv  15907  prodfdiv  15950  fprodf1o  16000  prodss  16001  fprodss  16002  fprodser  16003  fprodcl2lem  16004  fprodmul  16014  fproddiv  16015  fprodn0  16033  iprodclim3  16054  fprodefsum  16148  iserodd  16894  prmreclem2  16976  vdwapf  17031  vdwlem4  17043  ramcl  17088  prmodvdslcmf  17106  prdsplusg  17510  prdsmulr  17511  prdsvsca  17512  mrcflem  17661  mreacs  17713  acsfn  17714  hofcllem  18313  hofcl  18314  yonedalem3a  18329  yonedalem4c  18332  yonedainv  18336  prdspjmhm  18887  pwsco1mhm  18890  pwsco2mhm  18891  gsumz  18894  gsumwspan  18904  smndex1gbas  18960  odf1o1  19641  odf1o2  19642  sylow2blem1  19689  mulgmhm  19896  mulgghm  19897  iscyggen2  19950  cyggenod  19953  iscyg3  19955  gsumzsplit  19996  gsumsplit2  19998  gsumconst  20003  gsummptshft  20005  gsummhm2  20008  gsummptmhm  20009  gsummptf1o  20032  gsum2dlem1  20039  gsum2dlem2  20040  gsum2d  20041  prdsgsum  20050  dprdfeq0  20093  dprdlub  20097  dprdz  20101  dprd2dlem1  20112  dprd2da  20113  srglmhm  20302  srgrmhm  20303  ringlghm  20394  ringrghm  20395  gsumdixp  20399  pwspjmhmmgpd  20408  pwsgprod  20410  lmodvsghm  21023  gsumfsum  21563  regsumfsum  21564  expmhm  21565  expghm  21604  evpmodpmf1o  21725  frlmgsum  21901  frlmsplit2  21902  frlmphl  21910  uvcff  21920  uvcresum  21922  snifpsrbag  22049  psrass1lem  22062  rhmpsrlem1  22069  rhmpsrlem2  22070  psrmulcllem  22074  psrlidm  22090  psrridm  22091  psrcom  22096  resspsrmul  22104  mvrf  22113  mplmon  22165  mplmonmul  22166  mplcoe1  22167  mplcoe5lem  22169  mplcoe5  22170  mplbas2  22172  psrbagsn  22193  evlslem4  22206  evlslem2  22209  evlslem3  22210  evlslem6  22211  evlslem1  22212  evlsval2  22217  evlsval3  22219  evlsvvvallem  22221  evlsvvval  22223  selvvvval  22272  psdcl  22303  psdmplcl  22304  psdmul  22308  psropprmul  22376  coe1mul2  22409  coe1tmmul2  22416  coe1tmmul  22417  ply1coe  22437  gsumsmonply1  22446  gsummoncoe1  22447  mamulid  22577  mamurid  22578  mdetunilem9  22756  mdetuni0  22757  mdetmul  22759  smadiadetlem3lem1  22802  m2cpmfo  22892  pmatcollpw1  22912  pmatcollpw3lem  22919  pmatcollpw3fi1lem2  22923  pm2mpcl  22933  mply1topmatcl  22941  mp2pm2mplem2  22943  mp2pm2mp  22947  pm2mpmhmlem2  22955  cayhamlem4  23024  pptbas  23144  tgrest  23295  resttopon  23297  rest0  23305  restfpw  23315  ordtbaslem  23324  ordtuni  23326  ordtrest  23338  cnpfval  23370  pnrmopn  23479  cncmp  23528  discmp  23534  1stcfb  23581  2ndcomap  23594  dis2ndc  23596  comppfsc  23668  kgencmp  23681  ptpjpre1  23707  ptpjcn  23747  ptcldmpt  23750  ptclsg  23751  dfac14  23754  xkoccn  23755  txcnp  23756  ptcnp  23758  uptx  23761  ptcn  23763  ptrescn  23775  xkoptsub  23790  xkoco1cn  23793  xkoco2cn  23794  cnmpt11  23799  pt1hmeo  23942  fbasrn  24020  trfilss  24025  trfg  24027  rnelfmlem  24088  flfcnp2  24143  fclscmpi  24165  alexsublem  24180  ptcmplem3  24190  symgtgp  24242  subgntr  24243  opnsubg  24244  clsnsg  24246  tgpconncomp  24249  eltsms  24269  haustsms  24272  tsmscls  24274  tsms0  24278  tsmsmhm  24282  tgptsmscls  24286  tsmssplit  24288  tsmsxplem1  24289  tsmsxplem2  24290  prdsdsf  24503  prdsxmetlem  24504  imasdsf1olem  24509  prdsbl  24627  stdbdxmet  24651  met1stc  24657  xrge0gsumle  24970  xrge0tsms  24971  cncfmpt2ss  25054  cnmptre  25065  evth  25097  evth2  25098  tcphcph  25375  rrxmval  25543  minveclem1  25562  minveclem3b  25566  iunmbl  25691  uniioombllem3  25723  ismbfcn2  25776  mbfeqalem1  25779  mbfeqalem2  25780  mbfss  25784  mbfmulc2re  25786  mbfneg  25788  mbfpos  25789  mbfposr  25790  mbfposb  25791  mbfadd  25799  mbfmulc2  25801  mbfsup  25802  mbfinf  25803  mbflimsup  25804  mbflimlem  25805  mbflim  25806  itg1climres  25852  mbfi1fseqlem3  25855  mbfi1fseqlem4  25856  mbfi1flimlem  25860  mbfi1flim  25861  mbfmullem2  25862  mbfmul  25864  itg2const2  25879  itg2seq  25880  itg2monolem1  25888  itg2monolem2  25889  itg2monolem3  25890  itg2mono  25891  itg2gt0  25898  itg2cnlem1  25899  itg2cnlem2  25900  itg2cn  25901  iblss  25943  itgitg1  25947  itgle  25948  itgeqa  25952  itgss3  25953  ibladdlem  25958  itgaddlem1  25961  iblabslem  25966  iblabs  25967  iblabsr  25968  iblmulc2  25969  itgmulc2lem1  25970  bddmulibl  25977  bddiblnc  25980  itggt0  25982  itgcn  25983  ellimc2  26015  limcmpt  26021  limcres  26024  limccnp  26029  limccnp2  26030  limcco  26031  perfdvf  26041  dvcnp2  26058  dvaddbr  26076  dvmulbr  26077  dvcjbr  26087  dvexp  26091  dvrec  26093  dvmptres3  26094  dvmptadd  26098  dvmptmul  26099  dvmptres2  26100  dvmptcmul  26102  dvmptcj  26106  dvmptntr  26109  dvmptco  26110  dvcnvlem  26114  dvef  26118  dvferm1  26123  dvferm2  26125  rolle  26128  dvlipcn  26132  dvle  26145  dvivth  26148  lhop1lem  26151  lhop1  26152  lhop2  26153  lhop  26154  dvfsumle  26159  dvfsumge  26160  dvmptrecl  26162  dvfsumlem2  26165  itgsubstlem  26186  itgpowd  26188  tdeglem4  26196  coe1mul3  26235  elply2  26332  plyf  26334  elplyd  26338  plypf1  26348  coeeq2  26378  coemullem  26386  coe1termlem  26394  dvply2g  26425  elqaalem2  26460  taylfvallem  26497  taylf  26500  tayl0  26501  taylpfval  26504  taylthlem1  26512  taylthlem2  26513  ulmcau  26534  ulmss  26536  ulmdvlem3  26541  mtest  26543  mtestbdd  26544  itgulm2  26548  dvradcnv  26560  pserulm  26561  pserdvlem2  26567  abelthlem9  26579  pige3ALT  26661  logtayl  26801  logccv  26804  loglesqrt  26902  leibpi  27083  rlimcnp  27106  rlimcnp2  27107  xrlimcnp  27109  efrlim  27110  dfef2  27111  o1cxp  27115  cxp2lim  27117  amgmlem  27130  lgamgulmlem2  27170  lgamgulmlem6  27174  lgamcvg2  27195  regamcl  27201  relgamcl  27202  basellem2  27222  basellem3  27223  sqff1o  27322  fsumvma  27353  dchrelbasd  27379  lgseisenlem3  27517  lgseisenlem4  27518  chpo1ub  27620  dchrisum0lem2a  27657  logsqvma2  27683  pnt2  27753  pnt  27754  incistruhgr  29395  minvecolem1  31192  hoaddcl  32076  homulcl  32077  cofmpt2  32945  mptiffisupp  33004  fpwrelmap  33044  gsummpt2d  33335  gsummptfsres  33340  gsummptf1od  33341  gsummptfsf1o  33346  gsumfs2d  33347  gsumzrsum  33351  gsummulsubdishift2  33355  gsummulsubdishift1s  33356  gsummulsubdishift2s  33357  xrge0tsmsd  33359  gsumwrd2dccat  33364  gsumvsca1  33512  gsumvsca2  33513  elrgspnlem1  33528  elrgspnlem2  33529  elrgspnlem3  33530  elrgspnlem4  33531  elrgspn  33532  elrgspnsubrunlem2  33534  elrspunidl  33702  elrspunsn  33703  ressply1evls1  33821  evl1deg2  33833  deg1prod  33839  selvascl  33873  selvply1rhmlem1  33876  extvfvcl  33892  evlextv  33898  mplvrpmga  33901  psrgsum  33904  psrmon  33905  psrmonmul  33906  psrmonprod  33908  esplyfvaln  33930  vietadeg1  33934  fedgmullem1  33985  fedgmullem2  33986  evls1fldgencl  34026  fldextrspunlsplem  34029  fldextrspunlsp  34030  extdgfialglem2  34049  ordtrestNEW  34277  esumf1o  34406  esumadd  34413  esumcst  34419  esumpfinval  34431  esumpcvgval  34434  esumcvg  34442  esumsup  34445  measinb  34577  measdivcst  34580  sitgclg  34698  dstfrvclim1  34834  gsumncl  34896  gsumnunsn  34897  fdvneggt  34953  fdvnegge  34955  itgexpif  34959  logdivsqrle  35003  indispconn  35692  cvxpconn  35700  cvmsss2  35732  cvmliftlem6  35748  cvmliftlem8  35750  mrsubcv  35968  mrsubff  35970  mrsubrn  35971  mrsubccat  35976  elmrsubrn  35978  msubrn  35987  msubff  35988  divcnvlin  36191  faclimlem2  36202  faclim  36204  faclim2  36206  knoppcnlem5  37052  knoppcnlem8  37055  knoppcnlem10  37057  knoppcnlem11  37058  curf  38215  finixpnum  38222  matunitlindflem1  38233  matunitlindflem2  38234  ptrest  38236  poimirlem17  38254  poimirlem20  38257  poimirlem24  38261  poimirlem30  38267  broucube  38271  mblfinlem2  38275  volsupnfl  38282  mbfposadd  38284  itg2addnclem2  38289  itg2gt0cn  38292  ibladdnclem  38293  itgaddnclem1  38295  itgaddnc  38297  iblabsnclem  38300  iblabsnc  38301  iblmulc2nc  38302  itgmulc2nclem1  38303  itgmulc2nclem2  38304  itgmulc2nc  38305  itgabsnc  38306  itggt0cn  38307  ftc1cnnc  38309  ftc1anclem1  38310  ftc1anclem2  38311  ftc1anclem3  38312  ftc1anclem4  38313  ftc1anclem5  38314  ftc1anclem6  38315  ftc1anclem7  38316  ftc1anclem8  38317  ftc1anc  38318  areacirclem4  38328  upixp  38346  totbndbnd  38406  prdsbnd  38410  cntotbnd  38413  rrnequiv  38452  lsatlss  39738  tendoplcl  41523  tendoicl  41538  aks4d1p1p5  42810  aks4d1p9  42823  hashscontpow  42857  sticksstones10  42890  sticksstones17  42898  sticksstones18  42899  unitscyglem1  42930  redvmptabs  43089  fimgmcyc  43272  evlsbagval  43288  evlselv  43291  fsuppind  43292  fsuppssind  43295  mhpind  43296  evlsmhpvvval  43297  mhphflem  43298  cmpfiiin  43398  mzpclall  43428  mzpindd  43447  fphpdo  43514  dnnumch3  43744  kelac1  43760  dfac21  43763  cantnfresb  44021  cantnf2  44022  tfsconcatrev  44045  rfovcnvf1od  44700  fsovfd  44708  fsovcnvlem  44709  clsk3nimkb  44736  mnringmulrcld  44922  expgrowth  45015  mptelpm  45864  mapss2  45892  monoord2xrv  46167  expcnfg  46277  clim1fr1  46287  sumnnodd  46316  limsupvaluz2  46422  supcnvlimsup  46424  climliminflimsupd  46485  liminfltlem  46488  cncfmptssg  46555  cncfcompt  46567  cxpcncf2  46583  dvsinax  46597  fperdvper  46603  dvcosax  46610  dvnmptdivc  46622  dvnprodlem2  46631  dvnprodlem3  46632  iblsplit  46650  itgcoscmulx  46653  itgiccshift  46664  itgperiod  46665  itgsbtaddcnst  46666  dirkerf  46781  dirkeritg  46786  hoidmvlelem1  47279  hoidmvlelem5  47283  ovnhoilem1  47285  ovnhoilem2  47286  ovnlecvr2  47294  ovncvr2  47295  hoidifhspf  47302  hspmbllem2  47311  opnvonmbllem2  47317  iccvonmbllem  47362  vonioolem1  47364  vonioolem2  47365  vonicclem1  47367  vonicclem2  47368  smfid  47436  cfsetsnfsetf  47762  funcringcsetcALTV2lem3  49024  funcringcsetclem3ALTV  49047  gsumlsscl  49127  ply1mulgsum  49137  lincfsuppcl  49160  linccl  49161  lincsum  49176  lincscmcl  49179  lcoss  49183  lincext1  49201  el0ldep  49213  lincresunit1  49224  lincresunit3  49228  lmod1zr  49240  fdivmptf  49288  refdivmptf  49289  1arymaptf  49388  aacllem  50568  amgmwlem  50569