Theorem fmpttd 7104

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ↦ cmpt 5201  ⟶wf 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-fun 6532  df-fn 6533  df-f 6534

This theorem is referenced by:  fmpt3d  7105  fliftrel  7300  fsetfocdm  8873  pw2f1olem  9088  mapxpen  9155  fsuppssov1  9394  fsuppmptif  9409  wdom2d  9592  cantnflem1d  9700  cantnflem1  9701  ac5num  10048  acni2  10058  infpwfien  10074  fin23lem39  10362  fin1a2lem12  10423  canthp1lem2  10665  wuncval2  10759  gruf  10823  monoord2  14049  seqf1o  14059  ccatcl  14590  swrdcl  14661  swrdwrdsymb  14678  revcl  14777  revlen  14778  ello1mpt  15535  lo1o12  15547  lo1eq  15582  rlimeq  15583  climmpt2  15587  climrecl  15597  climge0  15598  o1compt  15601  rlimcn1b  15603  rlimdiv  15660  isercoll2  15683  caurcvg2  15692  fsumf1o  15737  sumss  15738  fsumss  15739  fsumcl2lem  15745  fsumadd  15754  isumclim3  15773  isummulc2  15776  fsummulc2  15798  fsumrelem  15821  climfsum  15834  isumshft  15853  divcnv  15867  prodfdiv  15910  fprodf1o  15960  prodss  15961  fprodss  15962  fprodser  15963  fprodcl2lem  15964  fprodmul  15974  fproddiv  15975  fprodn0  15993  iprodclim3  16014  fprodefsum  16109  iserodd  16853  prmreclem2  16935  vdwapf  16990  vdwlem4  17002  ramcl  17047  prmodvdslcmf  17065  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  mrcflem  17616  mreacs  17668  acsfn  17669  hofcllem  18268  hofcl  18269  yonedalem3a  18284  yonedalem4c  18287  yonedainv  18291  prdspjmhm  18805  pwsco1mhm  18808  pwsco2mhm  18809  gsumz  18812  gsumwspan  18822  odf1o1  19551  odf1o2  19552  sylow2blem1  19599  mulgmhm  19806  mulgghm  19807  iscyggen2  19860  cyggenod  19863  iscyg3  19865  gsumzsplit  19906  gsumsplit2  19908  gsumconst  19913  gsummptshft  19915  gsummhm2  19918  gsummptmhm  19919  gsummptf1o  19942  gsum2dlem1  19949  gsum2dlem2  19950  gsum2d  19951  prdsgsum  19960  dprdfeq0  20003  dprdlub  20007  dprdz  20011  dprd2dlem1  20022  dprd2da  20023  srglmhm  20179  srgrmhm  20180  ringlghm  20270  ringrghm  20271  gsumdixp  20277  pwspjmhmmgpd  20286  lmodvsghm  20878  gsumfsum  21400  regsumfsum  21401  expmhm  21402  expghm  21434  evpmodpmf1o  21554  frlmgsum  21730  frlmsplit2  21731  frlmphl  21739  uvcff  21749  uvcresum  21751  snifpsrbag  21878  psrass1lem  21890  rhmpsrlem1  21898  rhmpsrlem2  21899  psrmulcllem  21903  psrlidm  21920  psrridm  21921  psrcom  21926  resspsrmul  21934  mvrf  21943  mplmon  21991  mplmonmul  21992  mplcoe1  21993  mplcoe5lem  21995  mplcoe5  21996  mplbas2  21998  psrbagsn  22019  evlslem4  22032  evlslem2  22035  evlslem3  22036  evlslem6  22037  evlslem1  22038  evlsval2  22043  psdcl  22097  psdmplcl  22098  psdmul  22102  psropprmul  22171  coe1mul2  22204  coe1tmmul2  22211  coe1tmmul  22212  ply1coe  22234  gsumsmonply1  22243  gsummoncoe1  22244  mamulid  22377  mamurid  22378  mdetunilem9  22556  mdetuni0  22557  mdetmul  22559  smadiadetlem3lem1  22602  m2cpmfo  22692  pmatcollpw1  22712  pmatcollpw3lem  22719  pmatcollpw3fi1lem2  22723  pm2mpcl  22733  mply1topmatcl  22741  mp2pm2mplem2  22743  mp2pm2mp  22747  pm2mpmhmlem2  22755  cayhamlem4  22824  pptbas  22944  tgrest  23095  resttopon  23097  rest0  23105  restfpw  23115  ordtbaslem  23124  ordtuni  23126  ordtrest  23138  cnpfval  23170  pnrmopn  23279  cncmp  23328  discmp  23334  1stcfb  23381  2ndcomap  23394  dis2ndc  23396  comppfsc  23468  kgencmp  23481  ptpjpre1  23507  ptpjcn  23547  ptcldmpt  23550  ptclsg  23551  dfac14  23554  xkoccn  23555  txcnp  23556  ptcnp  23558  uptx  23561  ptcn  23563  ptrescn  23575  xkoptsub  23590  xkoco1cn  23593  xkoco2cn  23594  cnmpt11  23599  pt1hmeo  23742  fbasrn  23820  trfilss  23825  trfg  23827  rnelfmlem  23888  flfcnp2  23943  fclscmpi  23965  alexsublem  23980  ptcmplem3  23990  symgtgp  24042  subgntr  24043  opnsubg  24044  clsnsg  24046  tgpconncomp  24049  eltsms  24069  haustsms  24072  tsmscls  24074  tsms0  24078  tsmsmhm  24082  tgptsmscls  24086  tsmssplit  24088  tsmsxplem1  24089  tsmsxplem2  24090  prdsdsf  24304  prdsxmetlem  24305  imasdsf1olem  24310  prdsbl  24428  stdbdxmet  24452  met1stc  24458  xrge0gsumle  24771  xrge0tsms  24772  cncfmpt2ss  24858  cnmptre  24870  evth  24907  evth2  24908  tcphcph  25187  rrxmval  25355  minveclem1  25374  minveclem3b  25378  iunmbl  25504  uniioombllem3  25536  ismbfcn2  25589  mbfeqalem1  25592  mbfeqalem2  25593  mbfss  25597  mbfmulc2re  25599  mbfneg  25601  mbfpos  25602  mbfposr  25603  mbfposb  25604  mbfadd  25612  mbfmulc2  25614  mbfsup  25615  mbfinf  25616  mbflimsup  25617  mbflimlem  25618  mbflim  25619  itg1climres  25665  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1flimlem  25673  mbfi1flim  25674  mbfmullem2  25675  mbfmul  25677  itg2const2  25692  itg2seq  25693  itg2monolem1  25701  itg2monolem2  25702  itg2monolem3  25703  itg2mono  25704  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  itg2cn  25714  iblss  25756  itgitg1  25760  itgle  25761  itgeqa  25765  itgss3  25766  ibladdlem  25771  itgaddlem1  25774  iblabslem  25779  iblabs  25780  iblabsr  25781  iblmulc2  25782  itgmulc2lem1  25783  bddmulibl  25790  bddiblnc  25793  itggt0  25795  itgcn  25796  ellimc2  25828  limcmpt  25834  limcres  25837  limccnp  25842  limccnp2  25843  limcco  25844  perfdvf  25854  dvcnp2  25871  dvcnp2OLD  25872  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcjbr  25903  dvexp  25907  dvrec  25909  dvmptres3  25910  dvmptadd  25914  dvmptmul  25915  dvmptres2  25916  dvmptcmul  25918  dvmptcj  25922  dvmptntr  25925  dvmptco  25926  dvcnvlem  25930  dvef  25934  dvferm1  25939  dvferm2  25941  rolle  25944  dvlipcn  25949  dvle  25962  dvivth  25965  lhop1lem  25968  lhop1  25969  lhop2  25970  lhop  25971  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvmptrecl  25980  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgsubstlem  26005  itgpowd  26007  tdeglem4  26015  coe1mul3  26054  elply2  26151  plyf  26153  elplyd  26157  plypf1  26167  coeeq2  26197  coemullem  26205  coe1termlem  26213  dvply2g  26242  dvply2gOLD  26243  elqaalem2  26278  taylfvallem  26315  taylf  26318  tayl0  26319  taylpfval  26322  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmcau  26354  ulmss  26356  ulmdvlem3  26361  mtest  26363  mtestbdd  26364  itgulm2  26368  dvradcnv  26380  pserulm  26381  pserdvlem2  26388  abelthlem9  26400  pige3ALT  26479  logtayl  26619  logccv  26622  loglesqrt  26721  leibpi  26902  rlimcnp  26925  rlimcnp2  26926  xrlimcnp  26928  efrlim  26929  efrlimOLD  26930  dfef2  26931  o1cxp  26935  cxp2lim  26937  amgmlem  26950  lgamgulmlem2  26990  lgamgulmlem6  26994  lgamcvg2  27015  regamcl  27021  relgamcl  27022  basellem2  27042  basellem3  27043  sqff1o  27142  fsumvma  27174  dchrelbasd  27200  lgseisenlem3  27338  lgseisenlem4  27339  chpo1ub  27441  dchrisum0lem2a  27478  logsqvma2  27504  pnt2  27574  pnt  27575  incistruhgr  29004  minvecolem1  30801  hoaddcl  31685  homulcl  31686  cofmpt2  32558  mptiffisupp  32616  fpwrelmap  32656  gsummpt2d  32989  gsummptfsf1o  32994  gsumfs2d  32995  gsumzrsum  32999  xrge0tsmsd  33002  gsumwrd2dccat  33007  gsumvsca1  33169  gsumvsca2  33170  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspn  33187  elrgspnsubrunlem2  33189  elrspunidl  33389  elrspunsn  33390  ressply1evls1  33524  evl1deg2  33536  fedgmullem1  33615  fedgmullem2  33616  evls1fldgencl  33657  fldextrspunlsplem  33660  fldextrspunlsp  33661  ordtrestNEW  33898  esumf1o  34027  esumadd  34034  esumcst  34040  esumpfinval  34052  esumpcvgval  34055  esumcvg  34063  esumsup  34066  measinb  34198  measdivcst  34201  sitgclg  34320  dstfrvclim1  34456  gsumncl  34518  gsumnunsn  34519  fdvneggt  34578  fdvnegge  34580  itgexpif  34584  logdivsqrle  34628  indispconn  35202  cvxpconn  35210  cvmsss2  35242  cvmliftlem6  35258  cvmliftlem8  35260  mrsubcv  35478  mrsubff  35480  mrsubrn  35481  mrsubccat  35486  elmrsubrn  35488  msubrn  35497  msubff  35498  divcnvlin  35696  faclimlem2  35707  faclim  35709  faclim2  35711  knoppcnlem5  36461  knoppcnlem8  36464  knoppcnlem10  36466  knoppcnlem11  36467  curf  37568  finixpnum  37575  matunitlindflem1  37586  matunitlindflem2  37587  ptrest  37589  poimirlem17  37607  poimirlem20  37610  poimirlem24  37614  poimirlem30  37620  broucube  37624  mblfinlem2  37628  volsupnfl  37635  mbfposadd  37637  itg2addnclem2  37642  itg2gt0cn  37645  ibladdnclem  37646  itgaddnclem1  37648  itgaddnc  37650  iblabsnclem  37653  iblabsnc  37654  iblmulc2nc  37655  itgmulc2nclem1  37656  itgmulc2nclem2  37657  itgmulc2nc  37658  itgabsnc  37659  itggt0cn  37660  ftc1cnnc  37662  ftc1anclem1  37663  ftc1anclem2  37664  ftc1anclem3  37665  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  areacirclem4  37681  upixp  37699  totbndbnd  37759  prdsbnd  37763  cntotbnd  37766  rrnequiv  37805  lsatlss  38960  tendoplcl  40746  tendoicl  40761  aks4d1p1p5  42034  aks4d1p9  42047  hashscontpow  42081  sticksstones10  42114  sticksstones17  42122  sticksstones18  42123  unitscyglem1  42154  redvmptabs  42350  fimgmcyc  42504  pwsgprod  42514  evlsval3  42529  evlsvvvallem  42531  evlsvvval  42533  evlsbagval  42536  selvvvval  42555  evlselv  42557  fsuppind  42560  fsuppssind  42563  mhpind  42564  evlsmhpvvval  42565  mhphflem  42566  cmpfiiin  42667  mzpclall  42697  mzpindd  42716  fphpdo  42787  dnnumch3  43018  kelac1  43034  dfac21  43037  cantnfresb  43295  cantnf2  43296  tfsconcatrev  43319  rfovcnvf1od  43975  fsovfd  43983  fsovcnvlem  43984  clsk3nimkb  44011  mnringmulrcld  44200  expgrowth  44307  mptelpm  45148  mapss2  45177  monoord2xrv  45458  expcnfg  45568  clim1fr1  45578  sumnnodd  45607  limsupvaluz2  45715  supcnvlimsup  45717  climliminflimsupd  45778  liminfltlem  45781  cncfmptssg  45848  cncfcompt  45860  cxpcncf2  45876  dvsinax  45890  fperdvper  45896  dvcosax  45903  dvnmptdivc  45915  dvnprodlem2  45924  dvnprodlem3  45925  iblsplit  45943  itgcoscmulx  45946  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  dirkerf  46074  dirkeritg  46079  hoidmvlelem1  46572  hoidmvlelem5  46576  ovnhoilem1  46578  ovnhoilem2  46579  ovnlecvr2  46587  ovncvr2  46588  hoidifhspf  46595  hspmbllem2  46604  opnvonmbllem2  46610  iccvonmbllem  46655  vonioolem1  46657  vonioolem2  46658  vonicclem1  46660  vonicclem2  46661  smfid  46729  cfsetsnfsetf  47035  funcringcsetcALTV2lem3  48215  funcringcsetclem3ALTV  48238  gsumlsscl  48303  ply1mulgsum  48314  lincfsuppcl  48337  linccl  48338  lincsum  48353  lincscmcl  48356  lcoss  48360  lincext1  48378  el0ldep  48390  lincresunit1  48401  lincresunit3  48405  lmod1zr  48417  fdivmptf  48469  refdivmptf  48470  1arymaptf  48569  aacllem  49613  amgmwlem  49614