Theorem fmpttd 7115

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ↦ cmpt 5185  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  fmpt3d  7116  fliftrel  7316  fsetfocdm  8884  curf  8891  pw2f1olem  9101  mapxpen  9163  fsuppssov1  9377  fsuppmptif  9392  wdom2d  9575  cantnflem1d  9690  cantnflem1  9691  ac5num  10116  acni2  10126  infpwfien  10142  fin23lem39  10429  fin1a2lem12  10490  canthp1lem2  10739  wuncval2  10833  gruf  10897  monoord2  14177  seqf1o  14187  ccatcl  14720  swrdcl  14794  swrdwrdsymb  14813  revcl  14911  revlen  14912  ello1mpt  15689  lo1o12  15701  lo1eq  15736  rlimeq  15737  climmpt2  15741  climrecl  15751  climge0  15752  o1compt  15755  rlimcn1b  15757  rlimdiv  15814  isercoll2  15837  caurcvg2  15846  fsumf1o  15890  sumss  15891  fsumss  15892  fsumcl2lem  15898  fsumadd  15907  isumclim3  15926  isummulc2  15929  fsummulc2  15951  fsumrelem  15975  climfsum  15988  isumshft  16009  divcnv  16023  prodfdiv  16066  fprodf1o  16114  prodss  16115  fprodss  16116  fprodser  16117  fprodcl2lem  16118  fprodmul  16128  fproddiv  16129  fprodn0  16147  iprodclim3  16168  fprodefsum  16262  iserodd  17014  prmreclem2  17096  vdwapf  17151  vdwlem4  17163  ramcl  17208  prmodvdslcmf  17226  prdsplusg  17630  prdsmulr  17631  prdsvsca  17632  mrcflem  17781  mreacs  17833  acsfn  17834  hofcllem  18433  hofcl  18434  yonedalem3a  18449  yonedalem4c  18452  yonedainv  18456  prdspjmhm  19026  pwsco1mhm  19029  pwsco2mhm  19030  gsumz  19033  gsumwspan  19043  smndex1gbas  19099  odf1o1  19787  odf1o2  19788  sylow2blem1  19835  mulgmhm  20042  mulgghm  20043  iscyggen2  20096  cyggenod  20099  iscyg3  20101  gsumzsplit  20142  gsumsplit2  20144  gsumconst  20149  gsummptshft  20151  gsummhm2  20154  gsummptmhm  20155  gsummptf1o  20178  gsum2dlem1  20185  gsum2dlem2  20186  gsum2d  20187  prdsgsum  20196  dprdfeq0  20239  dprdlub  20243  dprdz  20247  dprd2dlem1  20258  dprd2da  20259  srglmhm  20448  srgrmhm  20449  ringlghm  20544  ringrghm  20545  gsumdixp  20549  pwspjmhmmgpd  20558  pwsgprod  20560  lmodvsghm  21199  gsumfsum  21741  regsumfsum  21742  expmhm  21743  expghm  21782  evpmodpmf1o  21903  frlmgsum  22079  frlmsplit2  22080  frlmphl  22088  uvcff  22098  uvcresum  22100  snifpsrbag  22229  psrass1lem  22242  rhmpsrlem1  22249  rhmpsrlem2  22250  psrmulcllem  22254  psrlidm  22270  psrridm  22271  psrcom  22276  resspsrmul  22284  mvrf  22293  mplmon  22345  mplmonmul  22346  mplcoe1  22347  mplcoe5lem  22349  mplcoe5  22350  mplbas2  22352  psrbagsn  22373  evlslem4  22386  evlslem2  22389  evlslem3  22390  evlslem6  22391  evlslem1  22392  evlsval2  22397  evlsval3  22399  evlsvvvallem  22401  evlsvvval  22403  selvvvval  22452  psdcl  22483  psdmplcl  22484  psdmul  22488  psropprmul  22556  coe1mul2  22589  coe1tmmul2  22596  coe1tmmul  22597  ply1coe  22617  gsumsmonply1  22626  gsummoncoe1  22627  mamulid  22757  mamurid  22758  mdetunilem9  22936  mdetuni0  22937  mdetmul  22939  smadiadetlem3lem1  22982  matunitlindflem1  22995  matunitlindflem2  22996  m2cpmfo  23075  pmatcollpw1  23095  pmatcollpw3lem  23102  pmatcollpw3fi1lem2  23106  pm2mpcl  23116  mply1topmatcl  23124  mp2pm2mplem2  23126  mp2pm2mp  23130  pm2mpmhmlem2  23138  cayhamlem4  23207  pptbas  23327  tgrest  23478  resttopon  23480  rest0  23488  restfpw  23498  ordtbaslem  23507  ordtuni  23509  ordtrest  23521  cnpfval  23553  pnrmopn  23662  cncmp  23711  discmp  23717  1stcfb  23764  2ndcomap  23778  dis2ndc  23780  comppfsc  23852  kgencmp  23865  ptpjpre1  23891  ptpjcn  23931  ptcldmpt  23934  ptclsg  23935  dfac14  23938  xkoccn  23939  txcnp  23940  ptcnp  23942  uptx  23945  ptcn  23947  ptrescn  23959  xkoptsub  23974  xkoco1cn  23977  xkoco2cn  23978  cnmpt11  23983  pt1hmeo  24126  fbasrn  24204  trfilss  24209  trfg  24211  rnelfmlem  24272  flfcnp2  24327  fclscmpi  24349  alexsublem  24364  ptcmplem3  24374  symgtgp  24426  subgntr  24427  opnsubg  24428  clsnsg  24430  tgpconncomp  24433  eltsms  24453  haustsms  24456  tsmscls  24458  tsms0  24462  tsmsmhm  24466  tgptsmscls  24470  tsmssplit  24472  tsmsxplem1  24473  tsmsxplem2  24474  prdsdsf  24687  prdsxmetlem  24688  imasdsf1olem  24693  prdsbl  24811  stdbdxmet  24835  met1stc  24841  xrge0gsumle  25154  xrge0tsms  25155  cncfmpt2ss  25238  cnmptre  25249  evth  25281  evth2  25282  tcphcph  25559  rrxmval  25727  minveclem1  25746  minveclem3b  25750  iunmbl  25875  uniioombllem3  25907  ismbfcn2  25960  mbfeqalem1  25963  mbfeqalem2  25964  mbfss  25968  mbfmulc2re  25970  mbfneg  25972  mbfpos  25973  mbfposr  25974  mbfposb  25975  mbfadd  25983  mbfmulc2  25985  mbfsup  25986  mbfinf  25987  mbflimsup  25988  mbflimlem  25989  mbflim  25990  itg1climres  26036  mbfi1fseqlem3  26039  mbfi1fseqlem4  26040  mbfi1flimlem  26044  mbfi1flim  26045  mbfmullem2  26046  mbfmul  26048  itg2const2  26063  itg2seq  26064  itg2monolem1  26072  itg2monolem2  26073  itg2monolem3  26074  itg2mono  26075  itg2gt0  26082  itg2cnlem1  26083  itg2cnlem2  26084  itg2cn  26085  iblss  26126  itgitg1  26130  itgle  26131  itgeqa  26135  itgss3  26136  ibladdlem  26141  itgaddlem1  26144  iblabslem  26149  iblabs  26150  iblabsr  26151  iblmulc2  26152  itgmulc2lem1  26153  bddmulibl  26160  bddiblnc  26163  itggt0  26165  itgcn  26166  ellimc2  26198  limcmpt  26204  limcres  26207  limccnp  26212  limccnp2  26213  limcco  26214  perfdvf  26224  dvcnp2  26241  dvaddbr  26259  dvmulbr  26260  dvcjbr  26270  dvexp  26274  dvrec  26276  dvmptres3  26277  dvmptadd  26281  dvmptmul  26282  dvmptres2  26283  dvmptcmul  26285  dvmptcj  26289  dvmptntr  26292  dvmptco  26293  dvcnvlem  26297  dvef  26301  dvferm1  26306  dvferm2  26308  rolle  26311  dvlipcn  26315  dvle  26328  dvivth  26331  lhop1lem  26334  lhop1  26335  lhop2  26336  lhop  26337  dvfsumle  26342  dvfsumge  26343  dvmptrecl  26345  dvfsumlem2  26348  itgsubstlem  26369  itgpowd  26371  tdeglem4  26379  coe1mul3  26418  elply2  26515  plyf  26517  elplyd  26521  plypf1  26532  coeeq2  26562  coemullem  26570  coe1termlem  26578  dvply2g  26607  elqaalem2  26644  taylfvallem  26686  taylf  26689  tayl0  26690  taylpfval  26693  taylthlem1  26701  taylthlem2  26702  ulmcau  26723  ulmss  26725  ulmdvlem3  26730  mtest  26732  mtestbdd  26733  itgulm2  26737  dvradcnv  26749  pserulm  26750  pserdvlem2  26756  abelthlem9  26768  pige3ALT  26849  logtayl  26989  logccv  26992  loglesqrt  27090  leibpi  27271  rlimcnp  27294  rlimcnp2  27295  xrlimcnp  27297  efrlim  27298  dfef2  27299  o1cxp  27303  cxp2lim  27305  amgmlem  27318  lgamgulmlem2  27358  lgamgulmlem6  27362  lgamcvg2  27383  regamcl  27389  relgamcl  27390  basellem2  27410  basellem3  27411  sqff1o  27510  fsumvma  27541  dchrelbasd  27567  lgseisenlem3  27705  lgseisenlem4  27706  chpo1ub  27808  dchrisum0lem2a  27845  logsqvma2  27871  pnt2  27941  pnt  27942  incistruhgr  29658  minvecolem1  31477  hoaddcl  32361  homulcl  32362  cofmpt2  33271  mptiffisupp  33329  fpwrelmap  33368  gsummpt2d  33653  gsummptfsres  33658  gsummptf1od  33659  gsummptfsf1o  33664  gsumfs2d  33665  gsumzrsum  33669  gsummulsubdishift2  33673  gsummulsubdishift1s  33674  gsummulsubdishift2s  33675  xrge0tsmsd  33677  gsumwrd2dccat  33682  gsumvsca1  33830  gsumvsca2  33831  elrgspnlem1  33846  elrgspnlem2  33847  elrgspnlem3  33848  elrgspnlem4  33849  elrgspn  33850  elrgspnsubrunlem2  33852  elrspunidl  34021  elrspunsn  34022  ressply1evls1  34140  evl1deg2  34152  deg1prod  34158  selvascl  34192  selvply1rhmlem1  34195  extvfvcl  34211  evlextv  34217  mplvrpmga  34220  psrgsum  34223  psrmon  34224  psrmonmul  34225  psrmonprod  34227  esplyfvaln  34249  vietadeg1  34253  fedgmullem1  34304  fedgmullem2  34305  evls1fldgencl  34345  fldextrspunlsplem  34348  fldextrspunlsp  34349  extdgfialglem2  34368  ordtrestNEW  34596  esumf1o  34725  esumadd  34732  esumcst  34738  esumpfinval  34750  esumpcvgval  34753  esumcvg  34761  esumsup  34764  measinb  34897  measdivcst  34900  sitgclg  35017  dstfrvclim1  35153  gsumncl  35215  gsumnunsn  35216  fdvneggt  35272  fdvnegge  35274  itgexpif  35278  logdivsqrle  35322  indispconn  36068  cvxpconn  36076  cvmsss2  36108  cvmliftlem6  36124  cvmliftlem8  36126  mrsubcv  36344  mrsubff  36346  mrsubrn  36347  mrsubccat  36352  elmrsubrn  36354  msubrn  36363  msubff  36364  divcnvlin  36573  faclimlem2  36584  faclim  36586  faclim2  36588  knoppcnlem5  37438  knoppcnlem8  37441  knoppcnlem10  37443  knoppcnlem11  37444  finixpnum  38604  ptrest  38613  poimirlem17  38631  poimirlem20  38634  poimirlem24  38638  poimirlem30  38644  broucube  38648  mblfinlem2  38652  volsupnfl  38659  mbfposadd  38661  itg2addnclem2  38666  itg2gt0cn  38669  ibladdnclem  38670  itgaddnclem1  38672  itgaddnc  38674  iblabsnclem  38677  iblabsnc  38678  iblmulc2nc  38679  itgmulc2nclem1  38680  itgmulc2nclem2  38681  itgmulc2nc  38682  itgabsnc  38683  itggt0cn  38684  ftc1cnnc  38686  ftc1anclem1  38687  ftc1anclem2  38688  ftc1anclem3  38689  ftc1anclem4  38690  ftc1anclem5  38691  ftc1anclem6  38692  ftc1anclem7  38693  ftc1anclem8  38694  ftc1anc  38695  areacirclem4  38705  upixp  38739  totbndbnd  38799  prdsbnd  38803  cntotbnd  38806  rrnequiv  38845  lsatlss  40129  tendoplcl  41914  tendoicl  41929  aks4d1p1p5  43201  aks4d1p9  43214  hashscontpow  43248  sticksstones10  43281  sticksstones17  43289  sticksstones18  43290  unitscyglem1  43321  redvmptabs  43487  fimgmcyc  43674  evlsbagval  43690  evlselv  43693  fsuppind  43694  fsuppssind  43697  mhpind  43698  evlsmhpvvval  43699  mhphflem  43700  cmpfiiin  43784  mzpclall  43814  mzpindd  43833  fphpdo  43900  dnnumch3  44130  kelac1  44141  dfac21  44144  cantnfresb  44402  cantnf2  44403  tfsconcatrev  44426  rfovcnvf1od  45080  fsovfd  45088  fsovcnvlem  45089  clsk3nimkb  45116  mnringmulrcld  45302  expgrowth  45395  mptelpm  46267  mapss2  46295  monoord2xrv  46569  expcnfg  46679  clim1fr1  46689  sumnnodd  46718  limsupvaluz2  46824  supcnvlimsup  46826  climliminflimsupd  46887  liminfltlem  46890  cncfmptssg  46957  cncfcompt  46969  cxpcncf2  46985  dvsinax  46999  fperdvper  47005  dvcosax  47012  dvnmptdivc  47024  dvnprodlem2  47033  dvnprodlem3  47034  iblsplit  47052  itgcoscmulx  47055  itgiccshift  47066  itgperiod  47067  itgsbtaddcnst  47068  dirkerf  47183  dirkeritg  47188  hoidmvlelem1  47681  hoidmvlelem5  47685  ovnhoilem1  47687  ovnhoilem2  47688  ovnlecvr2  47696  ovncvr2  47697  hoidifhspf  47704  hspmbllem2  47713  opnvonmbllem2  47719  iccvonmbllem  47764  vonioolem1  47766  vonioolem2  47767  vonicclem1  47769  vonicclem2  47770  smfid  47838  tmachlem-tpcomp  48024  tmachlem-tpopen  48027  cfsetsnfsetf  48204  funcringcsetcALTV2lem3  49465  funcringcsetclem3ALTV  49488  gsumlsscl  49568  ply1mulgsum  49578  lincfsuppcl  49601  linccl  49602  lincsum  49617  lincscmcl  49620  lcoss  49624  lincext1  49642  el0ldep  49654  lincresunit1  49665  lincresunit3  49669  lmod1zr  49681  fdivmptf  49729  refdivmptf  49730  1arymaptf  49829  aacllem  51015  crosspcld  51035  veronesefvcl  51048  veroquadgsumlem  51059  veroquadmodzerod  51060  amgmwlem  51063