Theorem fmpttd 7068

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

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

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 5232  ax-pr 5376

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 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6501  df-fn 6502  df-f 6503

This theorem is referenced by:  fmpt3d  7069  fliftrel  7263  fsetfocdm  8808  pw2f1olem  9019  mapxpen  9081  fsuppssov1  9297  fsuppmptif  9312  wdom2d  9495  cantnflem1d  9609  cantnflem1  9610  ac5num  9958  acni2  9968  infpwfien  9984  fin23lem39  10272  fin1a2lem12  10333  canthp1lem2  10576  wuncval2  10670  gruf  10734  monoord2  13995  seqf1o  14005  ccatcl  14536  swrdcl  14608  swrdwrdsymb  14625  revcl  14723  revlen  14724  ello1mpt  15483  lo1o12  15495  lo1eq  15530  rlimeq  15531  climmpt2  15535  climrecl  15545  climge0  15546  o1compt  15549  rlimcn1b  15551  rlimdiv  15608  isercoll2  15631  caurcvg2  15640  fsumf1o  15685  sumss  15686  fsumss  15687  fsumcl2lem  15693  fsumadd  15702  isumclim3  15721  isummulc2  15724  fsummulc2  15746  fsumrelem  15770  climfsum  15783  isumshft  15804  divcnv  15818  prodfdiv  15861  fprodf1o  15911  prodss  15912  fprodss  15913  fprodser  15914  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodn0  15944  iprodclim3  15965  fprodefsum  16060  iserodd  16806  prmreclem2  16888  vdwapf  16943  vdwlem4  16955  ramcl  17000  prmodvdslcmf  17018  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  mrcflem  17572  mreacs  17624  acsfn  17625  hofcllem  18224  hofcl  18225  yonedalem3a  18240  yonedalem4c  18243  yonedainv  18247  prdspjmhm  18797  pwsco1mhm  18800  pwsco2mhm  18801  gsumz  18804  gsumwspan  18814  smndex1gbas  18870  odf1o1  19547  odf1o2  19548  sylow2blem1  19595  mulgmhm  19802  mulgghm  19803  iscyggen2  19856  cyggenod  19859  iscyg3  19861  gsumzsplit  19902  gsumsplit2  19904  gsumconst  19909  gsummptshft  19911  gsummhm2  19914  gsummptmhm  19915  gsummptf1o  19938  gsum2dlem1  19945  gsum2dlem2  19946  gsum2d  19947  prdsgsum  19956  dprdfeq0  19999  dprdlub  20003  dprdz  20007  dprd2dlem1  20018  dprd2da  20019  srglmhm  20202  srgrmhm  20203  ringlghm  20293  ringrghm  20294  gsumdixp  20298  pwspjmhmmgpd  20307  pwsgprod  20309  lmodvsghm  20918  gsumfsum  21414  regsumfsum  21415  expmhm  21416  expghm  21455  evpmodpmf1o  21576  frlmgsum  21752  frlmsplit2  21753  frlmphl  21761  uvcff  21771  uvcresum  21773  snifpsrbag  21900  psrass1lem  21912  rhmpsrlem1  21919  rhmpsrlem2  21920  psrmulcllem  21924  psrlidm  21940  psrridm  21941  psrcom  21946  resspsrmul  21954  mvrf  21963  mplmon  22013  mplmonmul  22014  mplcoe1  22015  mplcoe5lem  22017  mplcoe5  22018  mplbas2  22020  psrbagsn  22041  evlslem4  22054  evlslem2  22057  evlslem3  22058  evlslem6  22059  evlslem1  22060  evlsval2  22065  evlsval3  22067  evlsvvvallem  22069  evlsvvval  22071  psdcl  22127  psdmplcl  22128  psdmul  22132  psropprmul  22201  coe1mul2  22234  coe1tmmul2  22241  coe1tmmul  22242  ply1coe  22263  gsumsmonply1  22272  gsummoncoe1  22273  mamulid  22406  mamurid  22407  mdetunilem9  22585  mdetuni0  22586  mdetmul  22588  smadiadetlem3lem1  22631  m2cpmfo  22721  pmatcollpw1  22741  pmatcollpw3lem  22748  pmatcollpw3fi1lem2  22752  pm2mpcl  22762  mply1topmatcl  22770  mp2pm2mplem2  22772  mp2pm2mp  22776  pm2mpmhmlem2  22784  cayhamlem4  22853  pptbas  22973  tgrest  23124  resttopon  23126  rest0  23134  restfpw  23144  ordtbaslem  23153  ordtuni  23155  ordtrest  23167  cnpfval  23199  pnrmopn  23308  cncmp  23357  discmp  23363  1stcfb  23410  2ndcomap  23423  dis2ndc  23425  comppfsc  23497  kgencmp  23510  ptpjpre1  23536  ptpjcn  23576  ptcldmpt  23579  ptclsg  23580  dfac14  23583  xkoccn  23584  txcnp  23585  ptcnp  23587  uptx  23590  ptcn  23592  ptrescn  23604  xkoptsub  23619  xkoco1cn  23622  xkoco2cn  23623  cnmpt11  23628  pt1hmeo  23771  fbasrn  23849  trfilss  23854  trfg  23856  rnelfmlem  23917  flfcnp2  23972  fclscmpi  23994  alexsublem  24009  ptcmplem3  24019  symgtgp  24071  subgntr  24072  opnsubg  24073  clsnsg  24075  tgpconncomp  24078  eltsms  24098  haustsms  24101  tsmscls  24103  tsms0  24107  tsmsmhm  24111  tgptsmscls  24115  tsmssplit  24117  tsmsxplem1  24118  tsmsxplem2  24119  prdsdsf  24332  prdsxmetlem  24333  imasdsf1olem  24338  prdsbl  24456  stdbdxmet  24480  met1stc  24486  xrge0gsumle  24799  xrge0tsms  24800  cncfmpt2ss  24883  cnmptre  24894  evth  24926  evth2  24927  tcphcph  25204  rrxmval  25372  minveclem1  25391  minveclem3b  25395  iunmbl  25520  uniioombllem3  25552  ismbfcn2  25605  mbfeqalem1  25608  mbfeqalem2  25609  mbfss  25613  mbfmulc2re  25615  mbfneg  25617  mbfpos  25618  mbfposr  25619  mbfposb  25620  mbfadd  25628  mbfmulc2  25630  mbfsup  25631  mbfinf  25632  mbflimsup  25633  mbflimlem  25634  mbflim  25635  itg1climres  25681  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1flimlem  25689  mbfi1flim  25690  mbfmullem2  25691  mbfmul  25693  itg2const2  25708  itg2seq  25709  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  itg2cn  25730  iblss  25772  itgitg1  25776  itgle  25777  itgeqa  25781  itgss3  25782  ibladdlem  25787  itgaddlem1  25790  iblabslem  25795  iblabs  25796  iblabsr  25797  iblmulc2  25798  itgmulc2lem1  25799  bddmulibl  25806  bddiblnc  25809  itggt0  25811  itgcn  25812  ellimc2  25844  limcmpt  25850  limcres  25853  limccnp  25858  limccnp2  25859  limcco  25860  perfdvf  25870  dvcnp2  25887  dvaddbr  25905  dvmulbr  25906  dvcjbr  25916  dvexp  25920  dvrec  25922  dvmptres3  25923  dvmptadd  25927  dvmptmul  25928  dvmptres2  25929  dvmptcmul  25931  dvmptcj  25935  dvmptntr  25938  dvmptco  25939  dvcnvlem  25943  dvef  25947  dvferm1  25952  dvferm2  25954  rolle  25957  dvlipcn  25961  dvle  25974  dvivth  25977  lhop1lem  25980  lhop1  25981  lhop2  25982  lhop  25983  dvfsumle  25988  dvfsumge  25989  dvmptrecl  25991  dvfsumlem2  25994  itgsubstlem  26015  itgpowd  26017  tdeglem4  26025  coe1mul3  26064  elply2  26161  plyf  26163  elplyd  26167  plypf1  26177  coeeq2  26207  coemullem  26215  coe1termlem  26223  dvply2g  26251  elqaalem2  26286  taylfvallem  26323  taylf  26326  tayl0  26327  taylpfval  26330  taylthlem1  26338  taylthlem2  26339  ulmcau  26360  ulmss  26362  ulmdvlem3  26367  mtest  26369  mtestbdd  26370  itgulm2  26374  dvradcnv  26386  pserulm  26387  pserdvlem2  26393  abelthlem9  26405  pige3ALT  26484  logtayl  26624  logccv  26627  loglesqrt  26725  leibpi  26906  rlimcnp  26929  rlimcnp2  26930  xrlimcnp  26932  efrlim  26933  dfef2  26934  o1cxp  26938  cxp2lim  26940  amgmlem  26953  lgamgulmlem2  26993  lgamgulmlem6  26997  lgamcvg2  27018  regamcl  27024  relgamcl  27025  basellem2  27045  basellem3  27046  sqff1o  27145  fsumvma  27176  dchrelbasd  27202  lgseisenlem3  27340  lgseisenlem4  27341  chpo1ub  27443  dchrisum0lem2a  27480  logsqvma2  27506  pnt2  27576  pnt  27577  incistruhgr  29148  minvecolem1  30945  hoaddcl  31829  homulcl  31830  cofmpt2  32707  mptiffisupp  32766  fpwrelmap  32806  gsummpt2d  33110  gsummptfsres  33115  gsummptf1od  33116  gsummptfsf1o  33121  gsumfs2d  33122  gsumzrsum  33126  gsummulsubdishift2  33130  gsummulsubdishift1s  33131  gsummulsubdishift2s  33132  xrge0tsmsd  33134  gsumwrd2dccat  33139  gsumvsca1  33287  gsumvsca2  33288  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  elrgspnsubrunlem2  33309  elrspunidl  33488  elrspunsn  33489  ressply1evls1  33625  evl1deg2  33637  deg1prod  33643  extvfvcl  33680  evlextv  33686  mplvrpmga  33689  psrgsum  33692  psrmon  33693  psrmonmul  33694  psrmonprod  33696  esplyfvaln  33718  vietadeg1  33722  fedgmullem1  33773  fedgmullem2  33774  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunlsp  33818  extdgfialglem2  33837  ordtrestNEW  34065  esumf1o  34194  esumadd  34201  esumcst  34207  esumpfinval  34219  esumpcvgval  34222  esumcvg  34230  esumsup  34233  measinb  34365  measdivcst  34368  sitgclg  34486  dstfrvclim1  34622  gsumncl  34684  gsumnunsn  34685  fdvneggt  34744  fdvnegge  34746  itgexpif  34750  logdivsqrle  34794  indispconn  35416  cvxpconn  35424  cvmsss2  35456  cvmliftlem6  35472  cvmliftlem8  35474  mrsubcv  35692  mrsubff  35694  mrsubrn  35695  mrsubccat  35700  elmrsubrn  35702  msubrn  35711  msubff  35712  divcnvlin  35915  faclimlem2  35926  faclim  35928  faclim2  35930  knoppcnlem5  36757  knoppcnlem8  36760  knoppcnlem10  36762  knoppcnlem11  36763  curf  37919  finixpnum  37926  matunitlindflem1  37937  matunitlindflem2  37938  ptrest  37940  poimirlem17  37958  poimirlem20  37961  poimirlem24  37965  poimirlem30  37971  broucube  37975  mblfinlem2  37979  volsupnfl  37986  mbfposadd  37988  itg2addnclem2  37993  itg2gt0cn  37996  ibladdnclem  37997  itgaddnclem1  37999  itgaddnc  38001  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  itgmulc2nclem1  38007  itgmulc2nclem2  38008  itgmulc2nc  38009  itgabsnc  38010  itggt0cn  38011  ftc1cnnc  38013  ftc1anclem1  38014  ftc1anclem2  38015  ftc1anclem3  38016  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  areacirclem4  38032  upixp  38050  totbndbnd  38110  prdsbnd  38114  cntotbnd  38117  rrnequiv  38156  lsatlss  39442  tendoplcl  41227  tendoicl  41242  aks4d1p1p5  42514  aks4d1p9  42527  hashscontpow  42561  sticksstones10  42594  sticksstones17  42602  sticksstones18  42603  unitscyglem1  42634  redvmptabs  42792  fimgmcyc  42979  evlsbagval  43002  selvvvval  43018  evlselv  43020  fsuppind  43023  fsuppssind  43026  mhpind  43027  evlsmhpvvval  43028  mhphflem  43029  cmpfiiin  43129  mzpclall  43159  mzpindd  43178  fphpdo  43245  dnnumch3  43475  kelac1  43491  dfac21  43494  cantnfresb  43752  cantnf2  43753  tfsconcatrev  43776  rfovcnvf1od  44431  fsovfd  44439  fsovcnvlem  44440  clsk3nimkb  44467  mnringmulrcld  44655  expgrowth  44762  mptelpm  45606  mapss2  45634  monoord2xrv  45911  expcnfg  46021  clim1fr1  46031  sumnnodd  46060  limsupvaluz2  46166  supcnvlimsup  46168  climliminflimsupd  46229  liminfltlem  46232  cncfmptssg  46299  cncfcompt  46311  cxpcncf2  46327  dvsinax  46341  fperdvper  46347  dvcosax  46354  dvnmptdivc  46366  dvnprodlem2  46375  dvnprodlem3  46376  iblsplit  46394  itgcoscmulx  46397  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  dirkerf  46525  dirkeritg  46530  hoidmvlelem1  47023  hoidmvlelem5  47027  ovnhoilem1  47029  ovnhoilem2  47030  ovnlecvr2  47038  ovncvr2  47039  hoidifhspf  47046  hspmbllem2  47055  opnvonmbllem2  47061  iccvonmbllem  47106  vonioolem1  47108  vonioolem2  47109  vonicclem1  47111  vonicclem2  47112  smfid  47180  cfsetsnfsetf  47500  funcringcsetcALTV2lem3  48762  funcringcsetclem3ALTV  48785  gsumlsscl  48850  ply1mulgsum  48860  lincfsuppcl  48883  linccl  48884  lincsum  48899  lincscmcl  48902  lcoss  48906  lincext1  48924  el0ldep  48936  lincresunit1  48947  lincresunit3  48951  lmod1zr  48963  fdivmptf  49011  refdivmptf  49012  1arymaptf  49111  aacllem  50270  amgmwlem  50271