Theorem fmpttd 7112

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ↦ cmpt 5231  ⟶wf 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-fun 6543  df-fn 6544  df-f 6545

This theorem is referenced by:  fmpt3d  7113  fliftrel  7302  pw2f1olem  9073  mapxpen  9140  fsuppmptif  9391  wdom2d  9572  cantnflem1d  9680  cantnflem1  9681  ac5num  10028  acni2  10038  infpwfien  10054  fin23lem39  10342  fin1a2lem12  10403  canthp1lem2  10645  wuncval2  10739  gruf  10803  monoord2  13996  seqf1o  14006  ccatcl  14521  swrdcl  14592  swrdwrdsymb  14609  revcl  14708  revlen  14709  ello1mpt  15462  lo1o12  15474  lo1eq  15509  rlimeq  15510  climmpt2  15514  climrecl  15524  climge0  15525  o1compt  15528  rlimcn1b  15530  rlimdiv  15589  isercoll2  15612  caurcvg2  15621  fsumf1o  15666  sumss  15667  fsumss  15668  fsumcl2lem  15674  fsumadd  15683  isumclim3  15702  isummulc2  15705  fsummulc2  15727  fsumrelem  15750  climfsum  15763  isumshft  15782  divcnv  15796  prodfdiv  15839  fprodf1o  15887  prodss  15888  fprodss  15889  fprodser  15890  fprodcl2lem  15891  fprodmul  15901  fproddiv  15902  fprodn0  15920  iprodclim3  15941  fprodefsum  16035  iserodd  16765  prmreclem2  16847  vdwapf  16902  vdwlem4  16914  ramcl  16959  prmodvdslcmf  16977  prdsplusg  17401  prdsmulr  17402  prdsvsca  17403  mrcflem  17547  mreacs  17599  acsfn  17600  hofcllem  18208  hofcl  18209  yonedalem3a  18224  yonedalem4c  18227  yonedainv  18231  prdspjmhm  18707  pwsco1mhm  18710  pwsco2mhm  18711  gsumz  18714  gsumwspan  18724  odf1o1  19435  odf1o2  19436  sylow2blem1  19483  mulgmhm  19690  mulgghm  19691  iscyggen2  19744  cyggenod  19747  iscyg3  19749  gsumzsplit  19790  gsumsplit2  19792  gsumconst  19797  gsummptshft  19799  gsummhm2  19802  gsummptmhm  19803  gsummptf1o  19826  gsum2dlem1  19833  gsum2dlem2  19834  gsum2d  19835  prdsgsum  19844  dprdfeq0  19887  dprdlub  19891  dprdz  19895  dprd2dlem1  19906  dprd2da  19907  srglmhm  20038  srgrmhm  20039  ringlghm  20118  ringrghm  20119  gsumdixp  20125  pwspjmhmmgpd  20135  lmodvsghm  20526  gsumfsum  21005  regsumfsum  21006  expmhm  21007  expghm  21037  evpmodpmf1o  21141  frlmgsum  21319  frlmsplit2  21320  frlmphl  21328  uvcff  21338  uvcresum  21340  snifpsrbag  21467  psrass1lemOLD  21485  psrass1lem  21488  psrmulcllem  21498  psrlidm  21515  psrridm  21516  psrcom  21521  resspsrmul  21529  mvrf  21536  mplmon  21582  mplmonmul  21583  mplcoe1  21584  mplcoe5lem  21586  mplcoe5  21587  mplbas2  21589  psrbagsn  21616  evlslem4  21629  evlslem2  21634  evlslem3  21635  evlslem6  21636  evlslem1  21637  evlsval2  21642  psropprmul  21752  coe1mul2  21783  coe1tmmul2  21790  coe1tmmul  21791  ply1coe  21812  gsumsmonply1  21819  gsummoncoe1  21820  mamulid  21935  mamurid  21936  mdetunilem9  22114  mdetuni0  22115  mdetmul  22117  smadiadetlem3lem1  22160  m2cpmfo  22250  pmatcollpw1  22270  pmatcollpw3lem  22277  pmatcollpw3fi1lem2  22281  pm2mpcl  22291  mply1topmatcl  22299  mp2pm2mplem2  22301  mp2pm2mp  22305  pm2mpmhmlem2  22313  cayhamlem4  22382  pptbas  22503  tgrest  22655  resttopon  22657  rest0  22665  restfpw  22675  ordtbaslem  22684  ordtuni  22686  ordtrest  22698  cnpfval  22730  pnrmopn  22839  cncmp  22888  discmp  22894  1stcfb  22941  2ndcomap  22954  dis2ndc  22956  comppfsc  23028  kgencmp  23041  ptpjpre1  23067  ptpjcn  23107  ptcldmpt  23110  ptclsg  23111  dfac14  23114  xkoccn  23115  txcnp  23116  ptcnp  23118  uptx  23121  ptcn  23123  ptrescn  23135  xkoptsub  23150  xkoco1cn  23153  xkoco2cn  23154  cnmpt11  23159  pt1hmeo  23302  fbasrn  23380  trfilss  23385  trfg  23387  rnelfmlem  23448  flfcnp2  23503  fclscmpi  23525  alexsublem  23540  ptcmplem3  23550  symgtgp  23602  subgntr  23603  opnsubg  23604  clsnsg  23606  tgpconncomp  23609  eltsms  23629  haustsms  23632  tsmscls  23634  tsms0  23638  tsmsmhm  23642  tgptsmscls  23646  tsmssplit  23648  tsmsxplem1  23649  tsmsxplem2  23650  prdsdsf  23865  prdsxmetlem  23866  imasdsf1olem  23871  prdsbl  23992  stdbdxmet  24016  met1stc  24022  xrge0gsumle  24341  xrge0tsms  24342  cncfmpt2ss  24424  cnmptre  24435  evth  24467  evth2  24468  tcphcph  24746  rrxmval  24914  minveclem1  24933  minveclem3b  24937  iunmbl  25062  uniioombllem3  25094  ismbfcn2  25147  mbfeqalem1  25150  mbfeqalem2  25151  mbfss  25155  mbfmulc2re  25157  mbfneg  25159  mbfpos  25160  mbfposr  25161  mbfposb  25162  mbfadd  25170  mbfmulc2  25172  mbfsup  25173  mbfinf  25174  mbflimsup  25175  mbflimlem  25176  mbflim  25177  itg1climres  25224  mbfi1fseqlem3  25227  mbfi1fseqlem4  25228  mbfi1flimlem  25232  mbfi1flim  25233  mbfmullem2  25234  mbfmul  25236  itg2const2  25251  itg2seq  25252  itg2monolem1  25260  itg2monolem2  25261  itg2monolem3  25262  itg2mono  25263  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  itg2cn  25273  iblss  25314  itgitg1  25318  itgle  25319  itgeqa  25323  itgss3  25324  ibladdlem  25329  itgaddlem1  25332  iblabslem  25337  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgmulc2lem1  25341  bddmulibl  25348  bddiblnc  25351  itggt0  25353  itgcn  25354  ellimc2  25386  limcmpt  25392  limcres  25395  limccnp  25400  limccnp2  25401  limcco  25402  perfdvf  25412  dvcnp2  25429  dvaddbr  25447  dvmulbr  25448  dvcjbr  25458  dvexp  25462  dvrec  25464  dvmptres3  25465  dvmptadd  25469  dvmptmul  25470  dvmptres2  25471  dvmptcmul  25473  dvmptcj  25477  dvmptntr  25480  dvmptco  25481  dvcnvlem  25485  dvef  25489  dvferm1  25494  dvferm2  25496  rolle  25499  dvlipcn  25503  dvle  25516  dvivth  25519  lhop1lem  25522  lhop1  25523  lhop2  25524  lhop  25525  dvfsumle  25530  dvfsumge  25531  dvmptrecl  25533  dvfsumlem2  25536  itgsubstlem  25557  itgpowd  25559  tdeglem4  25569  tdeglem4OLD  25570  coe1mul3  25609  elply2  25702  plyf  25704  elplyd  25708  plypf1  25718  coeeq2  25748  coemullem  25756  coe1termlem  25764  dvply2g  25790  elqaalem2  25825  taylfvallem  25862  taylf  25865  tayl0  25866  taylpfval  25869  taylthlem1  25877  taylthlem2  25878  ulmcau  25899  ulmss  25901  ulmdvlem3  25906  mtest  25908  mtestbdd  25909  itgulm2  25913  dvradcnv  25925  pserulm  25926  pserdvlem2  25932  abelthlem9  25944  pige3ALT  26021  logtayl  26160  logccv  26163  loglesqrt  26256  leibpi  26437  rlimcnp  26460  rlimcnp2  26461  xrlimcnp  26463  efrlim  26464  dfef2  26465  o1cxp  26469  cxp2lim  26471  amgmlem  26484  lgamgulmlem2  26524  lgamgulmlem6  26528  lgamcvg2  26549  regamcl  26555  relgamcl  26556  basellem2  26576  basellem3  26577  sqff1o  26676  fsumvma  26706  dchrelbasd  26732  lgseisenlem3  26870  lgseisenlem4  26871  chpo1ub  26973  dchrisum0lem2a  27010  logsqvma2  27036  pnt2  27106  pnt  27107  incistruhgr  28329  minvecolem1  30115  hoaddcl  30999  homulcl  31000  cofmpt2  31846  mptiffisupp  31903  fpwrelmap  31946  gsummpt2d  32189  xrge0tsmsd  32197  gsumvsca1  32359  gsumvsca2  32360  elrspunidl  32535  elrspunsn  32536  fedgmullem1  32703  fedgmullem2  32704  ordtrestNEW  32890  esumf1o  33037  esumadd  33044  esumcst  33050  esumpfinval  33062  esumpcvgval  33065  esumcvg  33073  esumsup  33076  measinb  33208  measdivcst  33211  sitgclg  33330  dstfrvclim1  33465  gsumncl  33540  gsumnunsn  33541  fdvneggt  33601  fdvnegge  33603  itgexpif  33607  logdivsqrle  33651  indispconn  34214  cvxpconn  34222  cvmsss2  34254  cvmliftlem6  34270  cvmliftlem8  34272  mrsubcv  34490  mrsubff  34492  mrsubrn  34493  mrsubccat  34498  elmrsubrn  34500  msubrn  34509  msubff  34510  divcnvlin  34691  faclimlem2  34703  faclim  34705  faclim2  34707  gg-dvcnp2  35163  gg-dvmulbr  35164  gg-dvfsumle  35171  gg-dvfsumlem2  35172  knoppcnlem5  35362  knoppcnlem8  35365  knoppcnlem10  35367  knoppcnlem11  35368  curf  36455  finixpnum  36462  matunitlindflem1  36473  matunitlindflem2  36474  ptrest  36476  poimirlem17  36494  poimirlem20  36497  poimirlem24  36501  poimirlem30  36507  broucube  36511  mblfinlem2  36515  volsupnfl  36522  mbfposadd  36524  itg2addnclem2  36529  itg2gt0cn  36532  ibladdnclem  36533  itgaddnclem1  36535  itgaddnc  36537  iblabsnclem  36540  iblabsnc  36541  iblmulc2nc  36542  itgmulc2nclem1  36543  itgmulc2nclem2  36544  itgmulc2nc  36545  itgabsnc  36546  itggt0cn  36547  ftc1cnnc  36549  ftc1anclem1  36550  ftc1anclem2  36551  ftc1anclem3  36552  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  areacirclem4  36568  upixp  36586  totbndbnd  36646  prdsbnd  36650  cntotbnd  36653  rrnequiv  36692  lsatlss  37855  tendoplcl  39641  tendoicl  39656  aks4d1p1p5  40929  aks4d1p9  40942  sticksstones10  40960  sticksstones17  40968  sticksstones18  40969  pwsgprod  41112  rhmmpllem1  41119  rhmmpllem2  41120  evlsval3  41129  evlsvvvallem  41131  evlsvvval  41133  evlsbagval  41136  selvvvval  41155  evlselv  41157  fsuppind  41160  fsuppssind  41163  mhpind  41164  evlsmhpvvval  41165  mhphflem  41166  cmpfiiin  41421  mzpclall  41451  mzpindd  41470  fphpdo  41541  dnnumch3  41775  kelac1  41791  dfac21  41794  cantnfresb  42060  cantnf2  42061  tfsconcatrev  42084  rfovcnvf1od  42741  fsovfd  42749  fsovcnvlem  42750  clsk3nimkb  42777  mnringmulrcld  42973  expgrowth  43080  mptelpm  43858  mapss2  43890  monoord2xrv  44181  expcnfg  44294  clim1fr1  44304  sumnnodd  44333  limsupvaluz2  44441  supcnvlimsup  44443  climliminflimsupd  44504  liminfltlem  44507  cncfmptssg  44574  cncfcompt  44586  cxpcncf2  44602  dvsinax  44616  fperdvper  44622  dvcosax  44629  dvnmptdivc  44641  dvnprodlem2  44650  dvnprodlem3  44651  iblsplit  44669  itgcoscmulx  44672  itgiccshift  44683  itgperiod  44684  itgsbtaddcnst  44685  dirkerf  44800  dirkeritg  44805  hoidmvlelem1  45298  hoidmvlelem5  45302  ovnhoilem1  45304  ovnhoilem2  45305  ovnlecvr2  45313  ovncvr2  45314  hoidifhspf  45321  hspmbllem2  45330  opnvonmbllem2  45336  iccvonmbllem  45381  vonioolem1  45383  vonioolem2  45384  vonicclem1  45386  vonicclem2  45387  smfid  45455  cfsetsnfsetf  45755  funcringcsetcALTV2lem3  46890  funcringcsetclem3ALTV  46913  gsumlsscl  47013  ply1mulgsum  47025  lincfsuppcl  47048  linccl  47049  lincsum  47064  lincscmcl  47067  lcoss  47071  lincext1  47089  el0ldep  47101  lincresunit1  47112  lincresunit3  47116  lmod1zr  47128  fdivmptf  47181  refdivmptf  47182  1arymaptf  47281  aacllem  47802  amgmwlem  47803