Theorem fmpttd 7111

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ↦ cmpt 5190  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  fmpt3d  7112  fliftrel  7312  fsetfocdm  8865  curf  8872  pw2f1olem  9082  mapxpen  9144  fsuppssov1  9357  fsuppmptif  9372  wdom2d  9555  cantnflem1d  9670  cantnflem1  9671  ac5num  10042  acni2  10052  infpwfien  10068  fin23lem39  10355  fin1a2lem12  10416  canthp1lem2  10665  wuncval2  10759  gruf  10823  monoord2  14099  seqf1o  14109  ccatcl  14641  swrdcl  14715  swrdwrdsymb  14734  revcl  14832  revlen  14833  ello1mpt  15610  lo1o12  15622  lo1eq  15657  rlimeq  15658  climmpt2  15662  climrecl  15672  climge0  15673  o1compt  15676  rlimcn1b  15678  rlimdiv  15735  isercoll2  15758  caurcvg2  15767  fsumf1o  15811  sumss  15812  fsumss  15813  fsumcl2lem  15819  fsumadd  15828  isumclim3  15847  isummulc2  15850  fsummulc2  15872  fsumrelem  15896  climfsum  15909  isumshft  15930  divcnv  15944  prodfdiv  15987  fprodf1o  16037  prodss  16038  fprodss  16039  fprodser  16040  fprodcl2lem  16041  fprodmul  16051  fproddiv  16052  fprodn0  16070  iprodclim3  16091  fprodefsum  16185  iserodd  16931  prmreclem2  17013  vdwapf  17068  vdwlem4  17080  ramcl  17125  prmodvdslcmf  17143  prdsplusg  17547  prdsmulr  17548  prdsvsca  17549  mrcflem  17698  mreacs  17750  acsfn  17751  hofcllem  18350  hofcl  18351  yonedalem3a  18366  yonedalem4c  18369  yonedainv  18373  prdspjmhm  18942  pwsco1mhm  18945  pwsco2mhm  18946  gsumz  18949  gsumwspan  18959  smndex1gbas  19015  odf1o1  19703  odf1o2  19704  sylow2blem1  19751  mulgmhm  19958  mulgghm  19959  iscyggen2  20012  cyggenod  20015  iscyg3  20017  gsumzsplit  20058  gsumsplit2  20060  gsumconst  20065  gsummptshft  20067  gsummhm2  20070  gsummptmhm  20071  gsummptf1o  20094  gsum2dlem1  20101  gsum2dlem2  20102  gsum2d  20103  prdsgsum  20112  dprdfeq0  20155  dprdlub  20159  dprdz  20163  dprd2dlem1  20174  dprd2da  20175  srglmhm  20364  srgrmhm  20365  ringlghm  20458  ringrghm  20459  gsumdixp  20463  pwspjmhmmgpd  20472  pwsgprod  20474  lmodvsghm  21111  gsumfsum  21651  regsumfsum  21652  expmhm  21653  expghm  21692  evpmodpmf1o  21813  frlmgsum  21989  frlmsplit2  21990  frlmphl  21998  uvcff  22008  uvcresum  22010  snifpsrbag  22139  psrass1lem  22152  rhmpsrlem1  22159  rhmpsrlem2  22160  psrmulcllem  22164  psrlidm  22180  psrridm  22181  psrcom  22186  resspsrmul  22194  mvrf  22203  mplmon  22255  mplmonmul  22256  mplcoe1  22257  mplcoe5lem  22259  mplcoe5  22260  mplbas2  22262  psrbagsn  22283  evlslem4  22296  evlslem2  22299  evlslem3  22300  evlslem6  22301  evlslem1  22302  evlsval2  22307  evlsval3  22309  evlsvvvallem  22311  evlsvvval  22313  selvvvval  22362  psdcl  22393  psdmplcl  22394  psdmul  22398  psropprmul  22466  coe1mul2  22499  coe1tmmul2  22506  coe1tmmul  22507  ply1coe  22527  gsumsmonply1  22536  gsummoncoe1  22537  mamulid  22667  mamurid  22668  mdetunilem9  22846  mdetuni0  22847  mdetmul  22849  smadiadetlem3lem1  22892  matunitlindflem1  22905  matunitlindflem2  22906  m2cpmfo  22985  pmatcollpw1  23005  pmatcollpw3lem  23012  pmatcollpw3fi1lem2  23016  pm2mpcl  23026  mply1topmatcl  23034  mp2pm2mplem2  23036  mp2pm2mp  23040  pm2mpmhmlem2  23048  cayhamlem4  23117  pptbas  23237  tgrest  23388  resttopon  23390  rest0  23398  restfpw  23408  ordtbaslem  23417  ordtuni  23419  ordtrest  23431  cnpfval  23463  pnrmopn  23572  cncmp  23621  discmp  23627  1stcfb  23674  2ndcomap  23688  dis2ndc  23690  comppfsc  23762  kgencmp  23775  ptpjpre1  23801  ptpjcn  23841  ptcldmpt  23844  ptclsg  23845  dfac14  23848  xkoccn  23849  txcnp  23850  ptcnp  23852  uptx  23855  ptcn  23857  ptrescn  23869  xkoptsub  23884  xkoco1cn  23887  xkoco2cn  23888  cnmpt11  23893  pt1hmeo  24036  fbasrn  24114  trfilss  24119  trfg  24121  rnelfmlem  24182  flfcnp2  24237  fclscmpi  24259  alexsublem  24274  ptcmplem3  24284  symgtgp  24336  subgntr  24337  opnsubg  24338  clsnsg  24340  tgpconncomp  24343  eltsms  24363  haustsms  24366  tsmscls  24368  tsms0  24372  tsmsmhm  24376  tgptsmscls  24380  tsmssplit  24382  tsmsxplem1  24383  tsmsxplem2  24384  prdsdsf  24597  prdsxmetlem  24598  imasdsf1olem  24603  prdsbl  24721  stdbdxmet  24745  met1stc  24751  xrge0gsumle  25064  xrge0tsms  25065  cncfmpt2ss  25148  cnmptre  25159  evth  25191  evth2  25192  tcphcph  25469  rrxmval  25637  minveclem1  25656  minveclem3b  25660  iunmbl  25785  uniioombllem3  25817  ismbfcn2  25870  mbfeqalem1  25873  mbfeqalem2  25874  mbfss  25878  mbfmulc2re  25880  mbfneg  25882  mbfpos  25883  mbfposr  25884  mbfposb  25885  mbfadd  25893  mbfmulc2  25895  mbfsup  25896  mbfinf  25897  mbflimsup  25898  mbflimlem  25899  mbflim  25900  itg1climres  25946  mbfi1fseqlem3  25949  mbfi1fseqlem4  25950  mbfi1flimlem  25954  mbfi1flim  25955  mbfmullem2  25956  mbfmul  25958  itg2const2  25973  itg2seq  25974  itg2monolem1  25982  itg2monolem2  25983  itg2monolem3  25984  itg2mono  25985  itg2gt0  25992  itg2cnlem1  25993  itg2cnlem2  25994  itg2cn  25995  iblss  26037  itgitg1  26041  itgle  26042  itgeqa  26046  itgss3  26047  ibladdlem  26052  itgaddlem1  26055  iblabslem  26060  iblabs  26061  iblabsr  26062  iblmulc2  26063  itgmulc2lem1  26064  bddmulibl  26071  bddiblnc  26074  itggt0  26076  itgcn  26077  ellimc2  26109  limcmpt  26115  limcres  26118  limccnp  26123  limccnp2  26124  limcco  26125  perfdvf  26135  dvcnp2  26152  dvaddbr  26170  dvmulbr  26171  dvcjbr  26181  dvexp  26185  dvrec  26187  dvmptres3  26188  dvmptadd  26192  dvmptmul  26193  dvmptres2  26194  dvmptcmul  26196  dvmptcj  26200  dvmptntr  26203  dvmptco  26204  dvcnvlem  26208  dvef  26212  dvferm1  26217  dvferm2  26219  rolle  26222  dvlipcn  26226  dvle  26239  dvivth  26242  lhop1lem  26245  lhop1  26246  lhop2  26247  lhop  26248  dvfsumle  26253  dvfsumge  26254  dvmptrecl  26256  dvfsumlem2  26259  itgsubstlem  26280  itgpowd  26282  tdeglem4  26290  coe1mul3  26329  elply2  26426  plyf  26428  elplyd  26432  plypf1  26442  coeeq2  26472  coemullem  26480  coe1termlem  26488  dvply2g  26519  elqaalem2  26554  taylfvallem  26594  taylf  26597  tayl0  26598  taylpfval  26601  taylthlem1  26609  taylthlem2  26610  ulmcau  26631  ulmss  26633  ulmdvlem3  26638  mtest  26640  mtestbdd  26641  itgulm2  26645  dvradcnv  26657  pserulm  26658  pserdvlem2  26664  abelthlem9  26676  pige3ALT  26758  logtayl  26898  logccv  26901  loglesqrt  26999  leibpi  27180  rlimcnp  27203  rlimcnp2  27204  xrlimcnp  27206  efrlim  27207  dfef2  27208  o1cxp  27212  cxp2lim  27214  amgmlem  27227  lgamgulmlem2  27267  lgamgulmlem6  27271  lgamcvg2  27292  regamcl  27298  relgamcl  27299  basellem2  27319  basellem3  27320  sqff1o  27419  fsumvma  27450  dchrelbasd  27476  lgseisenlem3  27614  lgseisenlem4  27615  chpo1ub  27717  dchrisum0lem2a  27754  logsqvma2  27780  pnt2  27850  pnt  27851  incistruhgr  29537  minvecolem1  31356  hoaddcl  32240  homulcl  32241  cofmpt2  33109  mptiffisupp  33167  fpwrelmap  33206  gsummpt2d  33491  gsummptfsres  33496  gsummptf1od  33497  gsummptfsf1o  33502  gsumfs2d  33503  gsumzrsum  33507  gsummulsubdishift2  33511  gsummulsubdishift1s  33512  gsummulsubdishift2s  33513  xrge0tsmsd  33515  gsumwrd2dccat  33520  gsumvsca1  33668  gsumvsca2  33669  elrgspnlem1  33684  elrgspnlem2  33685  elrgspnlem3  33686  elrgspnlem4  33687  elrgspn  33688  elrgspnsubrunlem2  33690  elrspunidl  33858  elrspunsn  33859  ressply1evls1  33977  evl1deg2  33989  deg1prod  33995  selvascl  34029  selvply1rhmlem1  34032  extvfvcl  34048  evlextv  34054  mplvrpmga  34057  psrgsum  34060  psrmon  34061  psrmonmul  34062  psrmonprod  34064  esplyfvaln  34086  vietadeg1  34090  fedgmullem1  34141  fedgmullem2  34142  evls1fldgencl  34182  fldextrspunlsplem  34185  fldextrspunlsp  34186  extdgfialglem2  34205  ordtrestNEW  34433  esumf1o  34562  esumadd  34569  esumcst  34575  esumpfinval  34587  esumpcvgval  34590  esumcvg  34598  esumsup  34601  measinb  34734  measdivcst  34737  sitgclg  34855  dstfrvclim1  34991  gsumncl  35053  gsumnunsn  35054  fdvneggt  35110  fdvnegge  35112  itgexpif  35116  logdivsqrle  35160  indispconn  35815  cvxpconn  35823  cvmsss2  35855  cvmliftlem6  35871  cvmliftlem8  35873  mrsubcv  36091  mrsubff  36093  mrsubrn  36094  mrsubccat  36099  elmrsubrn  36101  msubrn  36110  msubff  36111  divcnvlin  36314  faclimlem2  36325  faclim  36327  faclim2  36329  knoppcnlem5  37196  knoppcnlem8  37199  knoppcnlem10  37201  knoppcnlem11  37202  finixpnum  38361  ptrest  38370  poimirlem17  38388  poimirlem20  38391  poimirlem24  38395  poimirlem30  38401  broucube  38405  mblfinlem2  38409  volsupnfl  38416  mbfposadd  38418  itg2addnclem2  38423  itg2gt0cn  38426  ibladdnclem  38427  itgaddnclem1  38429  itgaddnc  38431  iblabsnclem  38434  iblabsnc  38435  iblmulc2nc  38436  itgmulc2nclem1  38437  itgmulc2nclem2  38438  itgmulc2nc  38439  itgabsnc  38440  itggt0cn  38441  ftc1cnnc  38443  ftc1anclem1  38444  ftc1anclem2  38445  ftc1anclem3  38446  ftc1anclem4  38447  ftc1anclem5  38448  ftc1anclem6  38449  ftc1anclem7  38450  ftc1anclem8  38451  ftc1anc  38452  areacirclem4  38462  upixp  38481  totbndbnd  38541  prdsbnd  38545  cntotbnd  38548  rrnequiv  38587  lsatlss  39871  tendoplcl  41656  tendoicl  41671  aks4d1p1p5  42943  aks4d1p9  42956  hashscontpow  42990  sticksstones10  43023  sticksstones17  43031  sticksstones18  43032  unitscyglem1  43063  redvmptabs  43237  fimgmcyc  43418  evlsbagval  43434  evlselv  43437  fsuppind  43438  fsuppssind  43441  mhpind  43442  evlsmhpvvval  43443  mhphflem  43444  cmpfiiin  43544  mzpclall  43574  mzpindd  43593  fphpdo  43660  dnnumch3  43890  kelac1  43906  dfac21  43909  cantnfresb  44167  cantnf2  44168  tfsconcatrev  44191  rfovcnvf1od  44846  fsovfd  44854  fsovcnvlem  44855  clsk3nimkb  44882  mnringmulrcld  45068  expgrowth  45161  mptelpm  46010  mapss2  46038  monoord2xrv  46313  expcnfg  46423  clim1fr1  46433  sumnnodd  46462  limsupvaluz2  46568  supcnvlimsup  46570  climliminflimsupd  46631  liminfltlem  46634  cncfmptssg  46701  cncfcompt  46713  cxpcncf2  46729  dvsinax  46743  fperdvper  46749  dvcosax  46756  dvnmptdivc  46768  dvnprodlem2  46777  dvnprodlem3  46778  iblsplit  46796  itgcoscmulx  46799  itgiccshift  46810  itgperiod  46811  itgsbtaddcnst  46812  dirkerf  46927  dirkeritg  46932  hoidmvlelem1  47425  hoidmvlelem5  47429  ovnhoilem1  47431  ovnhoilem2  47432  ovnlecvr2  47440  ovncvr2  47441  hoidifhspf  47448  hspmbllem2  47457  opnvonmbllem2  47463  iccvonmbllem  47508  vonioolem1  47510  vonioolem2  47511  vonicclem1  47513  vonicclem2  47514  smfid  47582  tmachlem-tpcomp  47768  tmachlem-tpopen  47771  cfsetsnfsetf  47948  funcringcsetcALTV2lem3  49209  funcringcsetclem3ALTV  49232  gsumlsscl  49312  ply1mulgsum  49322  lincfsuppcl  49345  linccl  49346  lincsum  49361  lincscmcl  49364  lcoss  49368  lincext1  49386  el0ldep  49398  lincresunit1  49409  lincresunit3  49413  lmod1zr  49425  fdivmptf  49473  refdivmptf  49474  1arymaptf  49573  aacllem  50774  crosspcld  50794  veronesefvcl  50807  veroquadgsumlem  50818  veroquadmodzerod  50819  amgmwlem  50822