Theorem fmpttd 7099

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ↦ cmpt 5224  ⟶wf 6528

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-fun 6534  df-fn 6535  df-f 6536

This theorem is referenced by:  fmpt3d  7100  fliftrel  7289  pw2f1olem  9059  mapxpen  9126  fsuppmptif  9376  wdom2d  9557  cantnflem1d  9665  cantnflem1  9666  ac5num  10013  acni2  10023  infpwfien  10039  fin23lem39  10327  fin1a2lem12  10388  canthp1lem2  10630  wuncval2  10724  gruf  10788  monoord2  13981  seqf1o  13991  ccatcl  14506  swrdcl  14577  swrdwrdsymb  14594  revcl  14693  revlen  14694  ello1mpt  15447  lo1o12  15459  lo1eq  15494  rlimeq  15495  climmpt2  15499  climrecl  15509  climge0  15510  o1compt  15513  rlimcn1b  15515  rlimdiv  15574  isercoll2  15597  caurcvg2  15606  fsumf1o  15651  sumss  15652  fsumss  15653  fsumcl2lem  15659  fsumadd  15668  isumclim3  15687  isummulc2  15690  fsummulc2  15712  fsumrelem  15735  climfsum  15748  isumshft  15767  divcnv  15781  prodfdiv  15824  fprodf1o  15872  prodss  15873  fprodss  15874  fprodser  15875  fprodcl2lem  15876  fprodmul  15886  fproddiv  15887  fprodn0  15905  iprodclim3  15926  fprodefsum  16020  iserodd  16750  prmreclem2  16832  vdwapf  16887  vdwlem4  16899  ramcl  16944  prmodvdslcmf  16962  prdsplusg  17386  prdsmulr  17387  prdsvsca  17388  mrcflem  17532  mreacs  17584  acsfn  17585  hofcllem  18193  hofcl  18194  yonedalem3a  18209  yonedalem4c  18212  yonedainv  18216  prdspjmhm  18685  pwsco1mhm  18688  pwsco2mhm  18689  gsumz  18692  gsumwspan  18702  odf1o1  19404  odf1o2  19405  sylow2blem1  19452  mulgmhm  19656  mulgghm  19657  iscyggen2  19708  cyggenod  19711  iscyg3  19713  gsumzsplit  19754  gsumsplit2  19756  gsumconst  19761  gsummptshft  19763  gsummhm2  19766  gsummptmhm  19767  gsummptf1o  19790  gsum2dlem1  19797  gsum2dlem2  19798  gsum2d  19799  prdsgsum  19808  dprdfeq0  19851  dprdlub  19855  dprdz  19859  dprd2dlem1  19870  dprd2da  19871  srglmhm  20002  srgrmhm  20003  ringlghm  20081  ringrghm  20082  gsumdixp  20086  pwspjmhmmgpd  20096  lmodvsghm  20482  gsumfsum  20946  regsumfsum  20947  expmhm  20948  expghm  20978  evpmodpmf1o  21082  frlmgsum  21260  frlmsplit2  21261  frlmphl  21269  uvcff  21279  uvcresum  21281  snifpsrbag  21406  psrass1lemOLD  21424  psrass1lem  21427  psrmulcllem  21437  psrlidm  21454  psrridm  21455  psrcom  21460  resspsrmul  21468  mvrf  21475  mplmon  21518  mplmonmul  21519  mplcoe1  21520  mplcoe5lem  21522  mplcoe5  21523  mplbas2  21525  psrbagsn  21553  evlslem4  21566  evlslem2  21571  evlslem3  21572  evlslem6  21573  evlslem1  21574  evlsval2  21579  psropprmul  21691  coe1mul2  21722  coe1tmmul2  21729  coe1tmmul  21730  ply1coe  21749  gsumsmonply1  21756  gsummoncoe1  21757  mamulid  21872  mamurid  21873  mdetunilem9  22051  mdetuni0  22052  mdetmul  22054  smadiadetlem3lem1  22097  m2cpmfo  22187  pmatcollpw1  22207  pmatcollpw3lem  22214  pmatcollpw3fi1lem2  22218  pm2mpcl  22228  mply1topmatcl  22236  mp2pm2mplem2  22238  mp2pm2mp  22242  pm2mpmhmlem2  22250  cayhamlem4  22319  pptbas  22440  tgrest  22592  resttopon  22594  rest0  22602  restfpw  22612  ordtbaslem  22621  ordtuni  22623  ordtrest  22635  cnpfval  22667  pnrmopn  22776  cncmp  22825  discmp  22831  1stcfb  22878  2ndcomap  22891  dis2ndc  22893  comppfsc  22965  kgencmp  22978  ptpjpre1  23004  ptpjcn  23044  ptcldmpt  23047  ptclsg  23048  dfac14  23051  xkoccn  23052  txcnp  23053  ptcnp  23055  uptx  23058  ptcn  23060  ptrescn  23072  xkoptsub  23087  xkoco1cn  23090  xkoco2cn  23091  cnmpt11  23096  pt1hmeo  23239  fbasrn  23317  trfilss  23322  trfg  23324  rnelfmlem  23385  flfcnp2  23440  fclscmpi  23462  alexsublem  23477  ptcmplem3  23487  symgtgp  23539  subgntr  23540  opnsubg  23541  clsnsg  23543  tgpconncomp  23546  eltsms  23566  haustsms  23569  tsmscls  23571  tsms0  23575  tsmsmhm  23579  tgptsmscls  23583  tsmssplit  23585  tsmsxplem1  23586  tsmsxplem2  23587  prdsdsf  23802  prdsxmetlem  23803  imasdsf1olem  23808  prdsbl  23929  stdbdxmet  23953  met1stc  23959  xrge0gsumle  24278  xrge0tsms  24279  cncfmpt2ss  24361  cnmptre  24372  evth  24404  evth2  24405  tcphcph  24683  rrxmval  24851  minveclem1  24870  minveclem3b  24874  iunmbl  24999  uniioombllem3  25031  ismbfcn2  25084  mbfeqalem1  25087  mbfeqalem2  25088  mbfss  25092  mbfmulc2re  25094  mbfneg  25096  mbfpos  25097  mbfposr  25098  mbfposb  25099  mbfadd  25107  mbfmulc2  25109  mbfsup  25110  mbfinf  25111  mbflimsup  25112  mbflimlem  25113  mbflim  25114  itg1climres  25161  mbfi1fseqlem3  25164  mbfi1fseqlem4  25165  mbfi1flimlem  25169  mbfi1flim  25170  mbfmullem2  25171  mbfmul  25173  itg2const2  25188  itg2seq  25189  itg2monolem1  25197  itg2monolem2  25198  itg2monolem3  25199  itg2mono  25200  itg2gt0  25207  itg2cnlem1  25208  itg2cnlem2  25209  itg2cn  25210  iblss  25251  itgitg1  25255  itgle  25256  itgeqa  25260  itgss3  25261  ibladdlem  25266  itgaddlem1  25269  iblabslem  25274  iblabs  25275  iblabsr  25276  iblmulc2  25277  itgmulc2lem1  25278  bddmulibl  25285  bddiblnc  25288  itggt0  25290  itgcn  25291  ellimc2  25323  limcmpt  25329  limcres  25332  limccnp  25337  limccnp2  25338  limcco  25339  perfdvf  25349  dvcnp2  25366  dvaddbr  25384  dvmulbr  25385  dvcjbr  25395  dvexp  25399  dvrec  25401  dvmptres3  25402  dvmptadd  25406  dvmptmul  25407  dvmptres2  25408  dvmptcmul  25410  dvmptcj  25414  dvmptntr  25417  dvmptco  25418  dvcnvlem  25422  dvef  25426  dvferm1  25431  dvferm2  25433  rolle  25436  dvlipcn  25440  dvle  25453  dvivth  25456  lhop1lem  25459  lhop1  25460  lhop2  25461  lhop  25462  dvfsumle  25467  dvfsumge  25468  dvmptrecl  25470  dvfsumlem2  25473  itgsubstlem  25494  itgpowd  25496  tdeglem4  25506  tdeglem4OLD  25507  coe1mul3  25546  elply2  25639  plyf  25641  elplyd  25645  plypf1  25655  coeeq2  25685  coemullem  25693  coe1termlem  25701  dvply2g  25727  elqaalem2  25762  taylfvallem  25799  taylf  25802  tayl0  25803  taylpfval  25806  taylthlem1  25814  taylthlem2  25815  ulmcau  25836  ulmss  25838  ulmdvlem3  25843  mtest  25845  mtestbdd  25846  itgulm2  25850  dvradcnv  25862  pserulm  25863  pserdvlem2  25869  abelthlem9  25881  pige3ALT  25958  logtayl  26097  logccv  26100  loglesqrt  26193  leibpi  26374  rlimcnp  26397  rlimcnp2  26398  xrlimcnp  26400  efrlim  26401  dfef2  26402  o1cxp  26406  cxp2lim  26408  amgmlem  26421  lgamgulmlem2  26461  lgamgulmlem6  26465  lgamcvg2  26486  regamcl  26492  relgamcl  26493  basellem2  26513  basellem3  26514  sqff1o  26613  fsumvma  26643  dchrelbasd  26669  lgseisenlem3  26807  lgseisenlem4  26808  chpo1ub  26910  dchrisum0lem2a  26947  logsqvma2  26973  pnt2  27043  pnt  27044  incistruhgr  28204  minvecolem1  29990  hoaddcl  30874  homulcl  30875  cofmpt2  31726  mptiffisupp  31786  fpwrelmap  31829  gsummpt2d  32072  xrge0tsmsd  32080  gsumvsca1  32242  gsumvsca2  32243  elrspunidl  32397  elrspunsn  32398  fedgmullem1  32552  fedgmullem2  32553  ordtrestNEW  32732  esumf1o  32879  esumadd  32886  esumcst  32892  esumpfinval  32904  esumpcvgval  32907  esumcvg  32915  esumsup  32918  measinb  33050  measdivcst  33053  sitgclg  33172  dstfrvclim1  33307  gsumncl  33382  gsumnunsn  33383  fdvneggt  33443  fdvnegge  33445  itgexpif  33449  logdivsqrle  33493  indispconn  34056  cvxpconn  34064  cvmsss2  34096  cvmliftlem6  34112  cvmliftlem8  34114  mrsubcv  34332  mrsubff  34334  mrsubrn  34335  mrsubccat  34340  elmrsubrn  34342  msubrn  34351  msubff  34352  divcnvlin  34532  faclimlem2  34544  faclim  34546  faclim2  34548  knoppcnlem5  35177  knoppcnlem8  35180  knoppcnlem10  35182  knoppcnlem11  35183  curf  36270  finixpnum  36277  matunitlindflem1  36288  matunitlindflem2  36289  ptrest  36291  poimirlem17  36309  poimirlem20  36312  poimirlem24  36316  poimirlem30  36322  broucube  36326  mblfinlem2  36330  volsupnfl  36337  mbfposadd  36339  itg2addnclem2  36344  itg2gt0cn  36347  ibladdnclem  36348  itgaddnclem1  36350  itgaddnc  36352  iblabsnclem  36355  iblabsnc  36356  iblmulc2nc  36357  itgmulc2nclem1  36358  itgmulc2nclem2  36359  itgmulc2nc  36360  itgabsnc  36361  itggt0cn  36362  ftc1cnnc  36364  ftc1anclem1  36365  ftc1anclem2  36366  ftc1anclem3  36367  ftc1anclem4  36368  ftc1anclem5  36369  ftc1anclem6  36370  ftc1anclem7  36371  ftc1anclem8  36372  ftc1anc  36373  areacirclem4  36383  upixp  36402  totbndbnd  36462  prdsbnd  36466  cntotbnd  36469  rrnequiv  36508  lsatlss  37671  tendoplcl  39457  tendoicl  39472  aks4d1p1p5  40745  aks4d1p9  40758  sticksstones10  40776  sticksstones17  40784  sticksstones18  40785  pwsgprod  40918  rhmmpllem1  40923  rhmmpllem2  40924  evlsval3  40930  evlsbagval  40934  fsuppind  40951  fsuppssind  40954  mhpind  40955  mhphflem  40956  mhphf  40957  cmpfiiin  41206  mzpclall  41236  mzpindd  41255  fphpdo  41326  dnnumch3  41560  kelac1  41576  dfac21  41579  cantnfresb  41845  cantnf2  41846  tfsconcatrev  41869  rfovcnvf1od  42526  fsovfd  42534  fsovcnvlem  42535  clsk3nimkb  42562  mnringmulrcld  42758  expgrowth  42865  mptelpm  43643  mapss2  43675  monoord2xrv  43967  expcnfg  44080  clim1fr1  44090  sumnnodd  44119  limsupvaluz2  44227  supcnvlimsup  44229  climliminflimsupd  44290  liminfltlem  44293  cncfmptssg  44360  cncfcompt  44372  cxpcncf2  44388  dvsinax  44402  fperdvper  44408  dvcosax  44415  dvnmptdivc  44427  dvnprodlem2  44436  dvnprodlem3  44437  iblsplit  44455  itgcoscmulx  44458  itgiccshift  44469  itgperiod  44470  itgsbtaddcnst  44471  dirkerf  44586  dirkeritg  44591  hoidmvlelem1  45084  hoidmvlelem5  45088  ovnhoilem1  45090  ovnhoilem2  45091  ovnlecvr2  45099  ovncvr2  45100  hoidifhspf  45107  hspmbllem2  45116  opnvonmbllem2  45122  iccvonmbllem  45167  vonioolem1  45169  vonioolem2  45170  vonicclem1  45172  vonicclem2  45173  smfid  45241  cfsetsnfsetf  45540  funcringcsetcALTV2lem3  46584  funcringcsetclem3ALTV  46607  gsumlsscl  46707  ply1mulgsum  46719  lincfsuppcl  46742  linccl  46743  lincsum  46758  lincscmcl  46761  lcoss  46765  lincext1  46783  el0ldep  46795  lincresunit1  46806  lincresunit3  46810  lmod1zr  46822  fdivmptf  46875  refdivmptf  46876  1arymaptf  46975  aacllem  47496  amgmwlem  47497