Theorem fmpttd 6998

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107   ↦ cmpt 5158  ⟶wf 6433

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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-fun 6439  df-fn 6440  df-f 6441

This theorem is referenced by:  fmpt3d  6999  fliftrel  7188  pw2f1olem  8872  mapxpen  8939  fsuppmptif  9167  wdom2d  9348  cantnflem1d  9455  cantnflem1  9456  ac5num  9801  acni2  9811  infpwfien  9827  fin23lem39  10115  fin1a2lem12  10176  canthp1lem2  10418  wuncval2  10512  gruf  10576  monoord2  13763  seqf1o  13773  ccatcl  14286  swrdcl  14367  swrdwrdsymb  14384  revcl  14483  revlen  14484  ello1mpt  15239  lo1o12  15251  lo1eq  15286  rlimeq  15287  climmpt2  15291  climrecl  15301  climge0  15302  o1compt  15305  rlimcn1b  15307  rlimdiv  15366  isercoll2  15389  caurcvg2  15398  fsumf1o  15444  sumss  15445  fsumss  15446  fsumcl2lem  15452  fsumadd  15461  isumclim3  15480  isummulc2  15483  fsummulc2  15505  fsumrelem  15528  climfsum  15541  isumshft  15560  divcnv  15574  prodfdiv  15617  fprodf1o  15665  prodss  15666  fprodss  15667  fprodser  15668  fprodcl2lem  15669  fprodmul  15679  fproddiv  15680  fprodn0  15698  iprodclim3  15719  fprodefsum  15813  iserodd  16545  prmreclem2  16627  vdwapf  16682  vdwlem4  16694  ramcl  16739  prmodvdslcmf  16757  prdsplusg  17178  prdsmulr  17179  prdsvsca  17180  mrcflem  17324  mreacs  17376  acsfn  17377  hofcllem  17985  hofcl  17986  yonedalem3a  18001  yonedalem4c  18004  yonedainv  18008  prdspjmhm  18476  pwsco1mhm  18479  pwsco2mhm  18480  gsumz  18483  gsumwspan  18494  odf1o1  19186  odf1o2  19187  sylow2blem1  19234  mulgmhm  19438  mulgghm  19439  iscyggen2  19490  cyggenod  19493  iscyg3  19495  gsumzsplit  19537  gsumsplit2  19539  gsumconst  19544  gsummptshft  19546  gsummhm2  19549  gsummptmhm  19550  gsummptf1o  19573  gsum2dlem1  19580  gsum2dlem2  19581  gsum2d  19582  prdsgsum  19591  dprdfeq0  19634  dprdlub  19638  dprdz  19642  dprd2dlem1  19653  dprd2da  19654  srglmhm  19780  srgrmhm  19781  ringlghm  19852  ringrghm  19853  gsumdixp  19857  lmodvsghm  20193  gsumfsum  20674  regsumfsum  20675  expmhm  20676  expghm  20706  evpmodpmf1o  20810  frlmgsum  20988  frlmsplit2  20989  frlmphl  20997  uvcff  21007  uvcresum  21009  snifpsrbag  21134  psrass1lemOLD  21152  psrass1lem  21155  psrmulcllem  21165  psrlidm  21181  psrridm  21182  psrcom  21187  resspsrmul  21195  mvrf  21202  mplmon  21245  mplmonmul  21246  mplcoe1  21247  mplcoe5lem  21249  mplcoe5  21250  mplbas2  21252  psrbagsn  21280  evlslem4  21293  evlslem2  21298  evlslem3  21299  evlslem6  21300  evlslem1  21301  evlsval2  21306  psropprmul  21418  coe1mul2  21449  coe1tmmul2  21456  coe1tmmul  21457  ply1coe  21476  gsumsmonply1  21483  gsummoncoe1  21484  mamulid  21599  mamurid  21600  mdetunilem9  21778  mdetuni0  21779  mdetmul  21781  smadiadetlem3lem1  21824  m2cpmfo  21914  pmatcollpw1  21934  pmatcollpw3lem  21941  pmatcollpw3fi1lem2  21945  pm2mpcl  21955  mply1topmatcl  21963  mp2pm2mplem2  21965  mp2pm2mp  21969  pm2mpmhmlem2  21977  cayhamlem4  22046  pptbas  22167  tgrest  22319  resttopon  22321  rest0  22329  restfpw  22339  ordtbaslem  22348  ordtuni  22350  ordtrest  22362  cnpfval  22394  pnrmopn  22503  cncmp  22552  discmp  22558  1stcfb  22605  2ndcomap  22618  dis2ndc  22620  comppfsc  22692  kgencmp  22705  ptpjpre1  22731  ptpjcn  22771  ptcldmpt  22774  ptclsg  22775  dfac14  22778  xkoccn  22779  txcnp  22780  ptcnp  22782  uptx  22785  ptcn  22787  ptrescn  22799  xkoptsub  22814  xkoco1cn  22817  xkoco2cn  22818  cnmpt11  22823  pt1hmeo  22966  fbasrn  23044  trfilss  23049  trfg  23051  rnelfmlem  23112  flfcnp2  23167  fclscmpi  23189  alexsublem  23204  ptcmplem3  23214  symgtgp  23266  subgntr  23267  opnsubg  23268  clsnsg  23270  tgpconncomp  23273  eltsms  23293  haustsms  23296  tsmscls  23298  tsms0  23302  tsmsmhm  23306  tgptsmscls  23310  tsmssplit  23312  tsmsxplem1  23313  tsmsxplem2  23314  prdsdsf  23529  prdsxmetlem  23530  imasdsf1olem  23535  prdsbl  23656  stdbdxmet  23680  met1stc  23686  xrge0gsumle  24005  xrge0tsms  24006  cncfmpt2ss  24088  cnmptre  24099  evth  24131  evth2  24132  tcphcph  24410  rrxmval  24578  minveclem1  24597  minveclem3b  24601  iunmbl  24726  uniioombllem3  24758  ismbfcn2  24811  mbfeqalem1  24814  mbfeqalem2  24815  mbfss  24819  mbfmulc2re  24821  mbfneg  24823  mbfpos  24824  mbfposr  24825  mbfposb  24826  mbfadd  24834  mbfmulc2  24836  mbfsup  24837  mbfinf  24838  mbflimsup  24839  mbflimlem  24840  mbflim  24841  itg1climres  24888  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1flimlem  24896  mbfi1flim  24897  mbfmullem2  24898  mbfmul  24900  itg2const2  24915  itg2seq  24916  itg2monolem1  24924  itg2monolem2  24925  itg2monolem3  24926  itg2mono  24927  itg2gt0  24934  itg2cnlem1  24935  itg2cnlem2  24936  itg2cn  24937  iblss  24978  itgitg1  24982  itgle  24983  itgeqa  24987  itgss3  24988  ibladdlem  24993  itgaddlem1  24996  iblabslem  25001  iblabs  25002  iblabsr  25003  iblmulc2  25004  itgmulc2lem1  25005  bddmulibl  25012  bddiblnc  25015  itggt0  25017  itgcn  25018  ellimc2  25050  limcmpt  25056  limcres  25059  limccnp  25064  limccnp2  25065  limcco  25066  perfdvf  25076  dvcnp2  25093  dvaddbr  25111  dvmulbr  25112  dvcjbr  25122  dvexp  25126  dvrec  25128  dvmptres3  25129  dvmptadd  25133  dvmptmul  25134  dvmptres2  25135  dvmptcmul  25137  dvmptcj  25141  dvmptntr  25144  dvmptco  25145  dvcnvlem  25149  dvef  25153  dvferm1  25158  dvferm2  25160  rolle  25163  dvlipcn  25167  dvle  25180  dvivth  25183  lhop1lem  25186  lhop1  25187  lhop2  25188  lhop  25189  dvfsumle  25194  dvfsumge  25195  dvmptrecl  25197  dvfsumlem2  25200  itgsubstlem  25221  itgpowd  25223  tdeglem4  25233  tdeglem4OLD  25234  coe1mul3  25273  elply2  25366  plyf  25368  elplyd  25372  plypf1  25382  coeeq2  25412  coemullem  25420  coe1termlem  25428  dvply2g  25454  elqaalem2  25489  taylfvallem  25526  taylf  25529  tayl0  25530  taylpfval  25533  taylthlem1  25541  taylthlem2  25542  ulmcau  25563  ulmss  25565  ulmdvlem3  25570  mtest  25572  mtestbdd  25573  itgulm2  25577  dvradcnv  25589  pserulm  25590  pserdvlem2  25596  abelthlem9  25608  pige3ALT  25685  logtayl  25824  logccv  25827  loglesqrt  25920  leibpi  26101  rlimcnp  26124  rlimcnp2  26125  xrlimcnp  26127  efrlim  26128  dfef2  26129  o1cxp  26133  cxp2lim  26135  amgmlem  26148  lgamgulmlem2  26188  lgamgulmlem6  26192  lgamcvg2  26213  regamcl  26219  relgamcl  26220  basellem2  26240  basellem3  26241  sqff1o  26340  fsumvma  26370  dchrelbasd  26396  lgseisenlem3  26534  lgseisenlem4  26535  chpo1ub  26637  dchrisum0lem2a  26674  logsqvma2  26700  pnt2  26770  pnt  26771  incistruhgr  27458  minvecolem1  29245  hoaddcl  30129  homulcl  30130  cofmpt2  30978  fpwrelmap  31077  gsummpt2d  31318  xrge0tsmsd  31326  gsumvsca1  31488  gsumvsca2  31489  elrspunidl  31615  fedgmullem1  31719  fedgmullem2  31720  ordtrestNEW  31880  esumf1o  32027  esumadd  32034  esumcst  32040  esumpfinval  32052  esumpcvgval  32055  esumcvg  32063  esumsup  32066  measinb  32198  measdivcst  32201  sitgclg  32318  dstfrvclim1  32453  gsumncl  32528  gsumnunsn  32529  fdvneggt  32589  fdvnegge  32591  itgexpif  32595  logdivsqrle  32639  indispconn  33205  cvxpconn  33213  cvmsss2  33245  cvmliftlem6  33261  cvmliftlem8  33263  mrsubcv  33481  mrsubff  33483  mrsubrn  33484  mrsubccat  33489  elmrsubrn  33491  msubrn  33500  msubff  33501  divcnvlin  33707  faclimlem2  33719  faclim  33721  faclim2  33723  knoppcnlem5  34686  knoppcnlem8  34689  knoppcnlem10  34691  knoppcnlem11  34692  curf  35764  finixpnum  35771  matunitlindflem1  35782  matunitlindflem2  35783  ptrest  35785  poimirlem17  35803  poimirlem20  35806  poimirlem24  35810  poimirlem30  35816  broucube  35820  mblfinlem2  35824  volsupnfl  35831  mbfposadd  35833  itg2addnclem2  35838  itg2gt0cn  35841  ibladdnclem  35842  itgaddnclem1  35844  itgaddnc  35846  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  itgmulc2nclem1  35852  itgmulc2nclem2  35853  itgmulc2nc  35854  itgabsnc  35855  itggt0cn  35856  ftc1cnnc  35858  ftc1anclem1  35859  ftc1anclem2  35860  ftc1anclem3  35861  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  areacirclem4  35877  upixp  35896  totbndbnd  35956  prdsbnd  35960  cntotbnd  35963  rrnequiv  36002  lsatlss  37017  tendoplcl  38802  tendoicl  38817  aks4d1p1p5  40090  aks4d1p9  40103  sticksstones10  40118  sticksstones17  40126  sticksstones18  40127  pwspjmhmmgpd  40274  pwsgprod  40276  evlsval3  40279  evlsbagval  40282  fsuppind  40286  fsuppssind  40289  mhpind  40290  mhphflem  40291  mhphf  40292  cmpfiiin  40526  mzpclall  40556  mzpindd  40575  fphpdo  40646  dnnumch3  40879  kelac1  40895  dfac21  40898  rfovcnvf1od  41619  fsovfd  41627  fsovcnvlem  41628  clsk3nimkb  41657  mnringmulrcld  41853  expgrowth  41960  mptelpm  42719  mapss2  42752  monoord2xrv  43031  expcnfg  43139  clim1fr1  43149  sumnnodd  43178  limsupvaluz2  43286  supcnvlimsup  43288  climliminflimsupd  43349  liminfltlem  43352  cncfmptssg  43419  cncfcompt  43431  cxpcncf2  43447  dvsinax  43461  fperdvper  43467  dvcosax  43474  dvnmptdivc  43486  dvnprodlem2  43495  dvnprodlem3  43496  iblsplit  43514  itgcoscmulx  43517  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  dirkerf  43645  dirkeritg  43650  hoidmvlelem1  44140  hoidmvlelem5  44144  ovnhoilem1  44146  ovnhoilem2  44147  ovnlecvr2  44155  ovncvr2  44156  hoidifhspf  44163  hspmbllem2  44172  opnvonmbllem2  44178  iccvonmbllem  44223  vonioolem1  44225  vonioolem2  44226  vonicclem1  44228  vonicclem2  44229  smfid  44297  cfsetsnfsetf  44563  funcringcsetcALTV2lem3  45607  funcringcsetclem3ALTV  45630  gsumlsscl  45730  ply1mulgsum  45742  lincfsuppcl  45765  linccl  45766  lincsum  45781  lincscmcl  45784  lcoss  45788  lincext1  45806  el0ldep  45818  lincresunit1  45829  lincresunit3  45833  lmod1zr  45845  fdivmptf  45898  refdivmptf  45899  1arymaptf  45998  aacllem  46516  amgmwlem  46517