Theorem fmpttd 7069

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

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

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fmpt3d  7070  fliftrel  7264  fsetfocdm  8810  pw2f1olem  9021  mapxpen  9083  fsuppssov1  9299  fsuppmptif  9314  wdom2d  9497  cantnflem1d  9609  cantnflem1  9610  ac5num  9958  acni2  9968  infpwfien  9984  fin23lem39  10272  fin1a2lem12  10333  canthp1lem2  10576  wuncval2  10670  gruf  10734  monoord2  13968  seqf1o  13978  ccatcl  14509  swrdcl  14581  swrdwrdsymb  14598  revcl  14696  revlen  14697  ello1mpt  15456  lo1o12  15468  lo1eq  15503  rlimeq  15504  climmpt2  15508  climrecl  15518  climge0  15519  o1compt  15522  rlimcn1b  15524  rlimdiv  15581  isercoll2  15604  caurcvg2  15613  fsumf1o  15658  sumss  15659  fsumss  15660  fsumcl2lem  15666  fsumadd  15675  isumclim3  15694  isummulc2  15697  fsummulc2  15719  fsumrelem  15742  climfsum  15755  isumshft  15774  divcnv  15788  prodfdiv  15831  fprodf1o  15881  prodss  15882  fprodss  15883  fprodser  15884  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodn0  15914  iprodclim3  15935  fprodefsum  16030  iserodd  16775  prmreclem2  16857  vdwapf  16912  vdwlem4  16924  ramcl  16969  prmodvdslcmf  16987  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  mrcflem  17541  mreacs  17593  acsfn  17594  hofcllem  18193  hofcl  18194  yonedalem3a  18209  yonedalem4c  18212  yonedainv  18216  prdspjmhm  18766  pwsco1mhm  18769  pwsco2mhm  18770  gsumz  18773  gsumwspan  18783  odf1o1  19513  odf1o2  19514  sylow2blem1  19561  mulgmhm  19768  mulgghm  19769  iscyggen2  19822  cyggenod  19825  iscyg3  19827  gsumzsplit  19868  gsumsplit2  19870  gsumconst  19875  gsummptshft  19877  gsummhm2  19880  gsummptmhm  19881  gsummptf1o  19904  gsum2dlem1  19911  gsum2dlem2  19912  gsum2d  19913  prdsgsum  19922  dprdfeq0  19965  dprdlub  19969  dprdz  19973  dprd2dlem1  19984  dprd2da  19985  srglmhm  20168  srgrmhm  20169  ringlghm  20259  ringrghm  20260  gsumdixp  20266  pwspjmhmmgpd  20275  pwsgprod  20277  lmodvsghm  20886  gsumfsum  21401  regsumfsum  21402  expmhm  21403  expghm  21442  evpmodpmf1o  21563  frlmgsum  21739  frlmsplit2  21740  frlmphl  21748  uvcff  21758  uvcresum  21760  snifpsrbag  21888  psrass1lem  21900  rhmpsrlem1  21908  rhmpsrlem2  21909  psrmulcllem  21913  psrlidm  21929  psrridm  21930  psrcom  21935  resspsrmul  21943  mvrf  21952  mplmon  22002  mplmonmul  22003  mplcoe1  22004  mplcoe5lem  22006  mplcoe5  22007  mplbas2  22009  psrbagsn  22030  evlslem4  22043  evlslem2  22046  evlslem3  22047  evlslem6  22048  evlslem1  22049  evlsval2  22054  evlsval3  22056  evlsvvvallem  22058  evlsvvval  22060  psdcl  22116  psdmplcl  22117  psdmul  22121  psropprmul  22190  coe1mul2  22223  coe1tmmul2  22230  coe1tmmul  22231  ply1coe  22254  gsumsmonply1  22263  gsummoncoe1  22264  mamulid  22397  mamurid  22398  mdetunilem9  22576  mdetuni0  22577  mdetmul  22579  smadiadetlem3lem1  22622  m2cpmfo  22712  pmatcollpw1  22732  pmatcollpw3lem  22739  pmatcollpw3fi1lem2  22743  pm2mpcl  22753  mply1topmatcl  22761  mp2pm2mplem2  22763  mp2pm2mp  22767  pm2mpmhmlem2  22775  cayhamlem4  22844  pptbas  22964  tgrest  23115  resttopon  23117  rest0  23125  restfpw  23135  ordtbaslem  23144  ordtuni  23146  ordtrest  23158  cnpfval  23190  pnrmopn  23299  cncmp  23348  discmp  23354  1stcfb  23401  2ndcomap  23414  dis2ndc  23416  comppfsc  23488  kgencmp  23501  ptpjpre1  23527  ptpjcn  23567  ptcldmpt  23570  ptclsg  23571  dfac14  23574  xkoccn  23575  txcnp  23576  ptcnp  23578  uptx  23581  ptcn  23583  ptrescn  23595  xkoptsub  23610  xkoco1cn  23613  xkoco2cn  23614  cnmpt11  23619  pt1hmeo  23762  fbasrn  23840  trfilss  23845  trfg  23847  rnelfmlem  23908  flfcnp2  23963  fclscmpi  23985  alexsublem  24000  ptcmplem3  24010  symgtgp  24062  subgntr  24063  opnsubg  24064  clsnsg  24066  tgpconncomp  24069  eltsms  24089  haustsms  24092  tsmscls  24094  tsms0  24098  tsmsmhm  24102  tgptsmscls  24106  tsmssplit  24108  tsmsxplem1  24109  tsmsxplem2  24110  prdsdsf  24323  prdsxmetlem  24324  imasdsf1olem  24329  prdsbl  24447  stdbdxmet  24471  met1stc  24477  xrge0gsumle  24790  xrge0tsms  24791  cncfmpt2ss  24877  cnmptre  24889  evth  24926  evth2  24927  tcphcph  25205  rrxmval  25373  minveclem1  25392  minveclem3b  25396  iunmbl  25522  uniioombllem3  25554  ismbfcn2  25607  mbfeqalem1  25610  mbfeqalem2  25611  mbfss  25615  mbfmulc2re  25617  mbfneg  25619  mbfpos  25620  mbfposr  25621  mbfposb  25622  mbfadd  25630  mbfmulc2  25632  mbfsup  25633  mbfinf  25634  mbflimsup  25635  mbflimlem  25636  mbflim  25637  itg1climres  25683  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1flimlem  25691  mbfi1flim  25692  mbfmullem2  25693  mbfmul  25695  itg2const2  25710  itg2seq  25711  itg2monolem1  25719  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  itg2cn  25732  iblss  25774  itgitg1  25778  itgle  25779  itgeqa  25783  itgss3  25784  ibladdlem  25789  itgaddlem1  25792  iblabslem  25797  iblabs  25798  iblabsr  25799  iblmulc2  25800  itgmulc2lem1  25801  bddmulibl  25808  bddiblnc  25811  itggt0  25813  itgcn  25814  ellimc2  25846  limcmpt  25852  limcres  25855  limccnp  25860  limccnp2  25861  limcco  25862  perfdvf  25872  dvcnp2  25889  dvcnp2OLD  25890  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcjbr  25921  dvexp  25925  dvrec  25927  dvmptres3  25928  dvmptadd  25932  dvmptmul  25933  dvmptres2  25934  dvmptcmul  25936  dvmptcj  25940  dvmptntr  25943  dvmptco  25944  dvcnvlem  25948  dvef  25952  dvferm1  25957  dvferm2  25959  rolle  25962  dvlipcn  25967  dvle  25980  dvivth  25983  lhop1lem  25986  lhop1  25987  lhop2  25988  lhop  25989  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvmptrecl  25998  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgsubstlem  26023  itgpowd  26025  tdeglem4  26033  coe1mul3  26072  elply2  26169  plyf  26171  elplyd  26175  plypf1  26185  coeeq2  26215  coemullem  26223  coe1termlem  26231  dvply2g  26260  dvply2gOLD  26261  elqaalem2  26296  taylfvallem  26333  taylf  26336  tayl0  26337  taylpfval  26340  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmcau  26372  ulmss  26374  ulmdvlem3  26379  mtest  26381  mtestbdd  26382  itgulm2  26386  dvradcnv  26398  pserulm  26399  pserdvlem2  26406  abelthlem9  26418  pige3ALT  26497  logtayl  26637  logccv  26640  loglesqrt  26739  leibpi  26920  rlimcnp  26943  rlimcnp2  26944  xrlimcnp  26946  efrlim  26947  efrlimOLD  26948  dfef2  26949  o1cxp  26953  cxp2lim  26955  amgmlem  26968  lgamgulmlem2  27008  lgamgulmlem6  27012  lgamcvg2  27033  regamcl  27039  relgamcl  27040  basellem2  27060  basellem3  27061  sqff1o  27160  fsumvma  27192  dchrelbasd  27218  lgseisenlem3  27356  lgseisenlem4  27357  chpo1ub  27459  dchrisum0lem2a  27496  logsqvma2  27522  pnt2  27592  pnt  27593  incistruhgr  29164  minvecolem1  30961  hoaddcl  31845  homulcl  31846  cofmpt2  32723  mptiffisupp  32782  fpwrelmap  32822  gsummpt2d  33142  gsummptfsres  33147  gsummptf1od  33148  gsummptfsf1o  33153  gsumfs2d  33154  gsumzrsum  33158  gsummulsubdishift2  33162  gsummulsubdishift1s  33163  gsummulsubdishift2s  33164  xrge0tsmsd  33166  gsumwrd2dccat  33171  gsumvsca1  33319  gsumvsca2  33320  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  elrgspn  33339  elrgspnsubrunlem2  33341  elrspunidl  33520  elrspunsn  33521  ressply1evls1  33657  evl1deg2  33669  deg1prod  33675  extvfvcl  33712  evlextv  33718  mplvrpmga  33721  psrgsum  33724  psrmon  33725  psrmonmul  33726  psrmonprod  33728  esplyfvaln  33750  vietadeg1  33754  fedgmullem1  33806  fedgmullem2  33807  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  extdgfialglem2  33870  ordtrestNEW  34098  esumf1o  34227  esumadd  34234  esumcst  34240  esumpfinval  34252  esumpcvgval  34255  esumcvg  34263  esumsup  34266  measinb  34398  measdivcst  34401  sitgclg  34519  dstfrvclim1  34655  gsumncl  34717  gsumnunsn  34718  fdvneggt  34777  fdvnegge  34779  itgexpif  34783  logdivsqrle  34827  indispconn  35447  cvxpconn  35455  cvmsss2  35487  cvmliftlem6  35503  cvmliftlem8  35505  mrsubcv  35723  mrsubff  35725  mrsubrn  35726  mrsubccat  35731  elmrsubrn  35733  msubrn  35742  msubff  35743  divcnvlin  35946  faclimlem2  35957  faclim  35959  faclim2  35961  knoppcnlem5  36716  knoppcnlem8  36719  knoppcnlem10  36721  knoppcnlem11  36722  curf  37838  finixpnum  37845  matunitlindflem1  37856  matunitlindflem2  37857  ptrest  37859  poimirlem17  37877  poimirlem20  37880  poimirlem24  37884  poimirlem30  37890  broucube  37894  mblfinlem2  37898  volsupnfl  37905  mbfposadd  37907  itg2addnclem2  37912  itg2gt0cn  37915  ibladdnclem  37916  itgaddnclem1  37918  itgaddnc  37920  iblabsnclem  37923  iblabsnc  37924  iblmulc2nc  37925  itgmulc2nclem1  37926  itgmulc2nclem2  37927  itgmulc2nc  37928  itgabsnc  37929  itggt0cn  37930  ftc1cnnc  37932  ftc1anclem1  37933  ftc1anclem2  37934  ftc1anclem3  37935  ftc1anclem4  37936  ftc1anclem5  37937  ftc1anclem6  37938  ftc1anclem7  37939  ftc1anclem8  37940  ftc1anc  37941  areacirclem4  37951  upixp  37969  totbndbnd  38029  prdsbnd  38033  cntotbnd  38036  rrnequiv  38075  lsatlss  39361  tendoplcl  41146  tendoicl  41161  aks4d1p1p5  42434  aks4d1p9  42447  hashscontpow  42481  sticksstones10  42514  sticksstones17  42522  sticksstones18  42523  unitscyglem1  42554  redvmptabs  42719  fimgmcyc  42893  evlsbagval  42916  selvvvval  42932  evlselv  42934  fsuppind  42937  fsuppssind  42940  mhpind  42941  evlsmhpvvval  42942  mhphflem  42943  cmpfiiin  43043  mzpclall  43073  mzpindd  43092  fphpdo  43163  dnnumch3  43393  kelac1  43409  dfac21  43412  cantnfresb  43670  cantnf2  43671  tfsconcatrev  43694  rfovcnvf1od  44349  fsovfd  44357  fsovcnvlem  44358  clsk3nimkb  44385  mnringmulrcld  44573  expgrowth  44680  mptelpm  45524  mapss2  45552  monoord2xrv  45830  expcnfg  45940  clim1fr1  45950  sumnnodd  45979  limsupvaluz2  46085  supcnvlimsup  46087  climliminflimsupd  46148  liminfltlem  46151  cncfmptssg  46218  cncfcompt  46230  cxpcncf2  46246  dvsinax  46260  fperdvper  46266  dvcosax  46273  dvnmptdivc  46285  dvnprodlem2  46294  dvnprodlem3  46295  iblsplit  46313  itgcoscmulx  46316  itgiccshift  46327  itgperiod  46328  itgsbtaddcnst  46329  dirkerf  46444  dirkeritg  46449  hoidmvlelem1  46942  hoidmvlelem5  46946  ovnhoilem1  46948  ovnhoilem2  46949  ovnlecvr2  46957  ovncvr2  46958  hoidifhspf  46965  hspmbllem2  46974  opnvonmbllem2  46980  iccvonmbllem  47025  vonioolem1  47027  vonioolem2  47028  vonicclem1  47030  vonicclem2  47031  smfid  47099  cfsetsnfsetf  47407  funcringcsetcALTV2lem3  48641  funcringcsetclem3ALTV  48664  gsumlsscl  48729  ply1mulgsum  48739  lincfsuppcl  48762  linccl  48763  lincsum  48778  lincscmcl  48781  lcoss  48785  lincext1  48803  el0ldep  48815  lincresunit1  48826  lincresunit3  48830  lmod1zr  48842  fdivmptf  48890  refdivmptf  48891  1arymaptf  48990  aacllem  50149  amgmwlem  50150