Theorem fmpttd 6879

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   ↦ cmpt 5146  ⟶wf 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363

This theorem is referenced by:  fmpt3d  6880  fliftrel  7061  pw2f1olem  8621  mapxpen  8683  fsuppmptif  8863  wdom2d  9044  cantnflem1d  9151  cantnflem1  9152  ac5num  9462  acni2  9472  infpwfien  9488  fin23lem39  9772  fin1a2lem12  9833  canthp1lem2  10075  wuncval2  10169  gruf  10233  monoord2  13402  seqf1o  13412  ccatcl  13926  swrdcl  14007  swrdwrdsymb  14024  revcl  14123  revlen  14124  ello1mpt  14878  lo1o12  14890  lo1eq  14925  rlimeq  14926  climmpt2  14930  climrecl  14940  climge0  14941  o1compt  14944  rlimcn1b  14946  rlimdiv  15002  isercoll2  15025  caurcvg2  15034  fsumf1o  15080  sumss  15081  fsumss  15082  fsumcl2lem  15088  fsumadd  15096  isumclim3  15114  isummulc2  15117  fsummulc2  15139  fsumrelem  15162  climfsum  15175  isumshft  15194  divcnv  15208  prodfdiv  15252  fprodf1o  15300  prodss  15301  fprodss  15302  fprodser  15303  fprodcl2lem  15304  fprodmul  15314  fproddiv  15315  fprodn0  15333  iprodclim3  15354  fprodefsum  15448  iserodd  16172  prmreclem2  16253  vdwapf  16308  vdwlem4  16320  ramcl  16365  prmodvdslcmf  16383  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  mrcflem  16877  mreacs  16929  acsfn  16930  hofcllem  17508  hofcl  17509  yonedalem3a  17524  yonedalem4c  17527  yonedainv  17531  prdspjmhm  17993  pwsco1mhm  17996  pwsco2mhm  17997  gsumz  18000  gsumwspan  18011  odf1o1  18697  odf1o2  18698  sylow2blem1  18745  mulgmhm  18948  mulgghm  18949  iscyggen2  19000  cyggenod  19003  iscyg3  19005  gsumzsplit  19047  gsumsplit2  19049  gsumconst  19054  gsummptshft  19056  gsummhm2  19059  gsummptmhm  19060  gsummptf1o  19083  gsum2dlem1  19090  gsum2dlem2  19091  gsum2d  19092  prdsgsum  19101  dprdfeq0  19144  dprdlub  19148  dprdz  19152  dprd2dlem1  19163  dprd2da  19164  srglmhm  19285  srgrmhm  19286  ringlghm  19354  ringrghm  19355  gsumdixp  19359  lmodvsghm  19695  snifpsrbag  20146  psrass1lem  20157  psrmulcllem  20167  psrlidm  20183  psrridm  20184  psrcom  20189  resspsrmul  20197  mvrf  20204  mplmon  20244  mplmonmul  20245  mplcoe1  20246  mplcoe5lem  20248  mplcoe5  20249  mplbas2  20251  psrbagsn  20275  evlslem4  20288  evlslem2  20292  evlslem3  20293  evlslem6  20294  evlslem1  20295  evlsval2  20300  psropprmul  20406  coe1mul2  20437  coe1tmmul2  20444  coe1tmmul  20445  ply1coe  20464  gsumsmonply1  20471  gsummoncoe1  20472  gsumfsum  20612  regsumfsum  20613  expmhm  20614  expghm  20643  evpmodpmf1o  20740  frlmgsum  20916  frlmsplit2  20917  frlmphl  20925  uvcff  20935  uvcresum  20937  mamulid  21050  mamurid  21051  mdetunilem9  21229  mdetuni0  21230  mdetmul  21232  smadiadetlem3lem1  21275  m2cpmfo  21364  pmatcollpw1  21384  pmatcollpw3lem  21391  pmatcollpw3fi1lem2  21395  pm2mpcl  21405  mply1topmatcl  21413  mp2pm2mplem2  21415  mp2pm2mp  21419  pm2mpmhmlem2  21427  cayhamlem4  21496  pptbas  21616  tgrest  21767  resttopon  21769  rest0  21777  restfpw  21787  ordtbaslem  21796  ordtuni  21798  ordtrest  21810  cnpfval  21842  pnrmopn  21951  cncmp  22000  discmp  22006  1stcfb  22053  2ndcomap  22066  dis2ndc  22068  comppfsc  22140  kgencmp  22153  ptpjpre1  22179  ptpjcn  22219  ptcldmpt  22222  ptclsg  22223  dfac14  22226  xkoccn  22227  txcnp  22228  ptcnp  22230  uptx  22233  ptcn  22235  ptrescn  22247  xkoptsub  22262  xkoco1cn  22265  xkoco2cn  22266  cnmpt11  22271  pt1hmeo  22414  fbasrn  22492  trfilss  22497  trfg  22499  rnelfmlem  22560  flfcnp2  22615  fclscmpi  22637  alexsublem  22652  ptcmplem3  22662  symgtgp  22714  subgntr  22715  opnsubg  22716  clsnsg  22718  tgpconncomp  22721  eltsms  22741  haustsms  22744  tsmscls  22746  tsms0  22750  tsmsmhm  22754  tgptsmscls  22758  tsmssplit  22760  tsmsxplem1  22761  tsmsxplem2  22762  prdsdsf  22977  prdsxmetlem  22978  imasdsf1olem  22983  prdsbl  23101  stdbdxmet  23125  met1stc  23131  xrge0gsumle  23441  xrge0tsms  23442  cncfmpt2ss  23523  cnmptre  23531  evth  23563  evth2  23564  tcphcph  23840  rrxmval  24008  minveclem1  24027  minveclem3b  24031  iunmbl  24154  uniioombllem3  24186  ismbfcn2  24239  mbfeqalem1  24242  mbfeqalem2  24243  mbfss  24247  mbfmulc2re  24249  mbfneg  24251  mbfpos  24252  mbfposr  24253  mbfposb  24254  mbfadd  24262  mbfmulc2  24264  mbfsup  24265  mbfinf  24266  mbflimsup  24267  mbflimlem  24268  mbflim  24269  itg1climres  24315  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1flimlem  24323  mbfi1flim  24324  mbfmullem2  24325  mbfmul  24327  itg2const2  24342  itg2seq  24343  itg2monolem1  24351  itg2monolem2  24352  itg2monolem3  24353  itg2mono  24354  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  itg2cn  24364  iblss  24405  itgitg1  24409  itgle  24410  itgeqa  24414  itgss3  24415  ibladdlem  24420  itgaddlem1  24423  iblabslem  24428  iblabs  24429  iblabsr  24430  iblmulc2  24431  itgmulc2lem1  24432  bddmulibl  24439  itggt0  24442  itgcn  24443  ellimc2  24475  limcmpt  24481  limcres  24484  limccnp  24489  limccnp2  24490  limcco  24491  perfdvf  24501  dvcnp2  24517  dvaddbr  24535  dvmulbr  24536  dvcjbr  24546  dvexp  24550  dvrec  24552  dvmptres3  24553  dvmptadd  24557  dvmptmul  24558  dvmptres2  24559  dvmptcmul  24561  dvmptcj  24565  dvmptntr  24568  dvmptco  24569  dvcnvlem  24573  dvef  24577  dvferm1  24582  dvferm2  24584  rolle  24587  dvlipcn  24591  dvle  24604  dvivth  24607  lhop1lem  24610  lhop1  24611  lhop2  24612  lhop  24613  dvfsumle  24618  dvfsumge  24619  dvmptrecl  24621  dvfsumlem2  24624  itgsubstlem  24645  tdeglem4  24654  coe1mul3  24693  elply2  24786  plyf  24788  elplyd  24792  plypf1  24802  coeeq2  24832  coemullem  24840  coe1termlem  24848  dvply2g  24874  elqaalem2  24909  taylfvallem  24946  taylf  24949  tayl0  24950  taylpfval  24953  taylthlem1  24961  taylthlem2  24962  ulmcau  24983  ulmss  24985  ulmdvlem3  24990  mtest  24992  mtestbdd  24993  itgulm2  24997  dvradcnv  25009  pserulm  25010  pserdvlem2  25016  abelthlem9  25028  pige3ALT  25105  logtayl  25243  logccv  25246  loglesqrt  25339  leibpi  25520  rlimcnp  25543  rlimcnp2  25544  xrlimcnp  25546  efrlim  25547  dfef2  25548  o1cxp  25552  cxp2lim  25554  amgmlem  25567  lgamgulmlem2  25607  lgamgulmlem6  25611  lgamcvg2  25632  regamcl  25638  relgamcl  25639  basellem2  25659  basellem3  25660  sqff1o  25759  fsumvma  25789  dchrelbasd  25815  lgseisenlem3  25953  lgseisenlem4  25954  chpo1ub  26056  dchrisum0lem2a  26093  logsqvma2  26119  pnt2  26189  pnt  26190  incistruhgr  26864  minvecolem1  28651  hoaddcl  29535  homulcl  29536  cofmpt2  30379  fpwrelmap  30469  gsummpt2d  30687  xrge0tsmsd  30692  gsumvsca1  30854  gsumvsca2  30855  fedgmullem1  31025  fedgmullem2  31026  ordtrestNEW  31164  esumf1o  31309  esumadd  31316  esumcst  31322  esumpfinval  31334  esumpcvgval  31337  esumcvg  31345  esumsup  31348  measinb  31480  measdivcst  31483  sitgclg  31600  dstfrvclim1  31735  gsumncl  31810  gsumnunsn  31811  fdvneggt  31871  fdvnegge  31873  itgexpif  31877  logdivsqrle  31921  indispconn  32481  cvxpconn  32489  cvmsss2  32521  cvmliftlem6  32537  cvmliftlem8  32539  mrsubcv  32757  mrsubff  32759  mrsubrn  32760  mrsubccat  32765  elmrsubrn  32767  msubrn  32776  msubff  32777  divcnvlin  32964  faclimlem2  32976  faclim  32978  faclim2  32980  knoppcnlem5  33836  knoppcnlem8  33839  knoppcnlem10  33841  knoppcnlem11  33842  curf  34885  finixpnum  34892  matunitlindflem1  34903  matunitlindflem2  34904  ptrest  34906  poimirlem17  34924  poimirlem20  34927  poimirlem24  34931  poimirlem30  34937  broucube  34941  mblfinlem2  34945  volsupnfl  34952  mbfposadd  34954  itg2addnclem2  34959  itg2gt0cn  34962  ibladdnclem  34963  itgaddnclem1  34965  itgaddnc  34967  iblabsnclem  34970  iblabsnc  34971  iblmulc2nc  34972  itgmulc2nclem1  34973  itgmulc2nclem2  34974  itgmulc2nc  34975  itgabsnc  34976  bddiblnc  34977  itggt0cn  34979  ftc1cnnc  34981  ftc1anclem1  34982  ftc1anclem2  34983  ftc1anclem3  34984  ftc1anclem4  34985  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  areacirclem4  35000  upixp  35019  totbndbnd  35082  prdsbnd  35086  cntotbnd  35089  rrnequiv  35128  lsatlss  36147  tendoplcl  37932  tendoicl  37947  cmpfiiin  39343  mzpclall  39373  mzpindd  39392  fphpdo  39463  dnnumch3  39696  kelac1  39712  dfac21  39715  itgpowd  39870  rfovcnvf1od  40399  fsovfd  40407  fsovcnvlem  40408  clsk3nimkb  40439  expgrowth  40716  mptelpm  41481  mapss2  41517  monoord2xrv  41809  expcnfg  41921  clim1fr1  41931  sumnnodd  41960  limsupvaluz2  42068  supcnvlimsup  42070  climliminflimsupd  42131  liminfltlem  42134  cncfmptssg  42202  cncfcompt  42215  cxpcncf2  42232  dvsinax  42246  fperdvper  42252  dvcosax  42260  dvnmptdivc  42272  dvnprodlem2  42281  dvnprodlem3  42282  iblsplit  42300  itgcoscmulx  42303  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  dirkerf  42431  dirkeritg  42436  hoidmvlelem1  42926  hoidmvlelem5  42930  ovnhoilem1  42932  ovnhoilem2  42933  ovnlecvr2  42941  ovncvr2  42942  hoidifhspf  42949  hspmbllem2  42958  opnvonmbllem2  42964  iccvonmbllem  43009  vonioolem1  43011  vonioolem2  43012  vonicclem1  43014  vonicclem2  43015  smfid  43078  funcringcsetcALTV2lem3  44358  funcringcsetclem3ALTV  44381  gsumlsscl  44480  ply1mulgsum  44493  lincfsuppcl  44517  linccl  44518  lincsum  44533  lincscmcl  44536  lcoss  44540  lincext1  44558  el0ldep  44570  lincresunit1  44581  lincresunit3  44585  lmod1zr  44597  fdivmptf  44650  refdivmptf  44651  aacllem  44951  amgmwlem  44952