Theorem fmpttd 7134

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   ↦ cmpt 5230  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  fmpt3d  7135  fliftrel  7327  fsetfocdm  8899  pw2f1olem  9114  mapxpen  9181  fsuppssov1  9421  fsuppmptif  9436  wdom2d  9617  cantnflem1d  9725  cantnflem1  9726  ac5num  10073  acni2  10083  infpwfien  10099  fin23lem39  10387  fin1a2lem12  10448  canthp1lem2  10690  wuncval2  10784  gruf  10848  monoord2  14070  seqf1o  14080  ccatcl  14608  swrdcl  14679  swrdwrdsymb  14696  revcl  14795  revlen  14796  ello1mpt  15553  lo1o12  15565  lo1eq  15600  rlimeq  15601  climmpt2  15605  climrecl  15615  climge0  15616  o1compt  15619  rlimcn1b  15621  rlimdiv  15678  isercoll2  15701  caurcvg2  15710  fsumf1o  15755  sumss  15756  fsumss  15757  fsumcl2lem  15763  fsumadd  15772  isumclim3  15791  isummulc2  15794  fsummulc2  15816  fsumrelem  15839  climfsum  15852  isumshft  15871  divcnv  15885  prodfdiv  15928  fprodf1o  15978  prodss  15979  fprodss  15980  fprodser  15981  fprodcl2lem  15982  fprodmul  15992  fproddiv  15993  fprodn0  16011  iprodclim3  16032  fprodefsum  16127  iserodd  16868  prmreclem2  16950  vdwapf  17005  vdwlem4  17017  ramcl  17062  prmodvdslcmf  17080  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  mrcflem  17650  mreacs  17702  acsfn  17703  hofcllem  18314  hofcl  18315  yonedalem3a  18330  yonedalem4c  18333  yonedainv  18337  prdspjmhm  18854  pwsco1mhm  18857  pwsco2mhm  18858  gsumz  18861  gsumwspan  18871  odf1o1  19604  odf1o2  19605  sylow2blem1  19652  mulgmhm  19859  mulgghm  19860  iscyggen2  19913  cyggenod  19916  iscyg3  19918  gsumzsplit  19959  gsumsplit2  19961  gsumconst  19966  gsummptshft  19968  gsummhm2  19971  gsummptmhm  19972  gsummptf1o  19995  gsum2dlem1  20002  gsum2dlem2  20003  gsum2d  20004  prdsgsum  20013  dprdfeq0  20056  dprdlub  20060  dprdz  20064  dprd2dlem1  20075  dprd2da  20076  srglmhm  20238  srgrmhm  20239  ringlghm  20325  ringrghm  20326  gsumdixp  20332  pwspjmhmmgpd  20341  lmodvsghm  20937  gsumfsum  21469  regsumfsum  21470  expmhm  21471  expghm  21503  evpmodpmf1o  21631  frlmgsum  21809  frlmsplit2  21810  frlmphl  21818  uvcff  21828  uvcresum  21830  snifpsrbag  21957  psrass1lem  21969  rhmpsrlem1  21977  rhmpsrlem2  21978  psrmulcllem  21982  psrlidm  21999  psrridm  22000  psrcom  22005  resspsrmul  22013  mvrf  22022  mplmon  22070  mplmonmul  22071  mplcoe1  22072  mplcoe5lem  22074  mplcoe5  22075  mplbas2  22077  psrbagsn  22104  evlslem4  22117  evlslem2  22120  evlslem3  22121  evlslem6  22122  evlslem1  22123  evlsval2  22128  psdcl  22182  psdmplcl  22183  psdmul  22187  psropprmul  22254  coe1mul2  22287  coe1tmmul2  22294  coe1tmmul  22295  ply1coe  22317  gsumsmonply1  22326  gsummoncoe1  22327  mamulid  22462  mamurid  22463  mdetunilem9  22641  mdetuni0  22642  mdetmul  22644  smadiadetlem3lem1  22687  m2cpmfo  22777  pmatcollpw1  22797  pmatcollpw3lem  22804  pmatcollpw3fi1lem2  22808  pm2mpcl  22818  mply1topmatcl  22826  mp2pm2mplem2  22828  mp2pm2mp  22832  pm2mpmhmlem2  22840  cayhamlem4  22909  pptbas  23030  tgrest  23182  resttopon  23184  rest0  23192  restfpw  23202  ordtbaslem  23211  ordtuni  23213  ordtrest  23225  cnpfval  23257  pnrmopn  23366  cncmp  23415  discmp  23421  1stcfb  23468  2ndcomap  23481  dis2ndc  23483  comppfsc  23555  kgencmp  23568  ptpjpre1  23594  ptpjcn  23634  ptcldmpt  23637  ptclsg  23638  dfac14  23641  xkoccn  23642  txcnp  23643  ptcnp  23645  uptx  23648  ptcn  23650  ptrescn  23662  xkoptsub  23677  xkoco1cn  23680  xkoco2cn  23681  cnmpt11  23686  pt1hmeo  23829  fbasrn  23907  trfilss  23912  trfg  23914  rnelfmlem  23975  flfcnp2  24030  fclscmpi  24052  alexsublem  24067  ptcmplem3  24077  symgtgp  24129  subgntr  24130  opnsubg  24131  clsnsg  24133  tgpconncomp  24136  eltsms  24156  haustsms  24159  tsmscls  24161  tsms0  24165  tsmsmhm  24169  tgptsmscls  24173  tsmssplit  24175  tsmsxplem1  24176  tsmsxplem2  24177  prdsdsf  24392  prdsxmetlem  24393  imasdsf1olem  24398  prdsbl  24519  stdbdxmet  24543  met1stc  24549  xrge0gsumle  24868  xrge0tsms  24869  cncfmpt2ss  24955  cnmptre  24967  evth  25004  evth2  25005  tcphcph  25284  rrxmval  25452  minveclem1  25471  minveclem3b  25475  iunmbl  25601  uniioombllem3  25633  ismbfcn2  25686  mbfeqalem1  25689  mbfeqalem2  25690  mbfss  25694  mbfmulc2re  25696  mbfneg  25698  mbfpos  25699  mbfposr  25700  mbfposb  25701  mbfadd  25709  mbfmulc2  25711  mbfsup  25712  mbfinf  25713  mbflimsup  25714  mbflimlem  25715  mbflim  25716  itg1climres  25763  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1flimlem  25771  mbfi1flim  25772  mbfmullem2  25773  mbfmul  25775  itg2const2  25790  itg2seq  25791  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  itg2cn  25812  iblss  25854  itgitg1  25858  itgle  25859  itgeqa  25863  itgss3  25864  ibladdlem  25869  itgaddlem1  25872  iblabslem  25877  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgmulc2lem1  25881  bddmulibl  25888  bddiblnc  25891  itggt0  25893  itgcn  25894  ellimc2  25926  limcmpt  25932  limcres  25935  limccnp  25940  limccnp2  25941  limcco  25942  perfdvf  25952  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcjbr  26001  dvexp  26005  dvrec  26007  dvmptres3  26008  dvmptadd  26012  dvmptmul  26013  dvmptres2  26014  dvmptcmul  26016  dvmptcj  26020  dvmptntr  26023  dvmptco  26024  dvcnvlem  26028  dvef  26032  dvferm1  26037  dvferm2  26039  rolle  26042  dvlipcn  26047  dvle  26060  dvivth  26063  lhop1lem  26066  lhop1  26067  lhop2  26068  lhop  26069  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvmptrecl  26078  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgsubstlem  26103  itgpowd  26105  tdeglem4  26113  coe1mul3  26152  elply2  26249  plyf  26251  elplyd  26255  plypf1  26265  coeeq2  26295  coemullem  26303  coe1termlem  26311  dvply2g  26340  dvply2gOLD  26341  elqaalem2  26376  taylfvallem  26413  taylf  26416  tayl0  26417  taylpfval  26420  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmcau  26452  ulmss  26454  ulmdvlem3  26459  mtest  26461  mtestbdd  26462  itgulm2  26466  dvradcnv  26478  pserulm  26479  pserdvlem2  26486  abelthlem9  26498  pige3ALT  26576  logtayl  26716  logccv  26719  loglesqrt  26818  leibpi  26999  rlimcnp  27022  rlimcnp2  27023  xrlimcnp  27025  efrlim  27026  efrlimOLD  27027  dfef2  27028  o1cxp  27032  cxp2lim  27034  amgmlem  27047  lgamgulmlem2  27087  lgamgulmlem6  27091  lgamcvg2  27112  regamcl  27118  relgamcl  27119  basellem2  27139  basellem3  27140  sqff1o  27239  fsumvma  27271  dchrelbasd  27297  lgseisenlem3  27435  lgseisenlem4  27436  chpo1ub  27538  dchrisum0lem2a  27575  logsqvma2  27601  pnt2  27671  pnt  27672  incistruhgr  29110  minvecolem1  30902  hoaddcl  31786  homulcl  31787  cofmpt2  32650  mptiffisupp  32707  fpwrelmap  32750  gsummpt2d  33034  gsummptfsf1o  33039  gsumfs2d  33040  gsumzrsum  33044  xrge0tsmsd  33047  gsumwrd2dccat  33052  gsumvsca1  33214  gsumvsca2  33215  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  elrspunidl  33435  elrspunsn  33436  evl1deg2  33581  fedgmullem1  33656  fedgmullem2  33657  evls1fldgencl  33694  ordtrestNEW  33881  esumf1o  34030  esumadd  34037  esumcst  34043  esumpfinval  34055  esumpcvgval  34058  esumcvg  34066  esumsup  34069  measinb  34201  measdivcst  34204  sitgclg  34323  dstfrvclim1  34458  gsumncl  34533  gsumnunsn  34534  fdvneggt  34593  fdvnegge  34595  itgexpif  34599  logdivsqrle  34643  indispconn  35218  cvxpconn  35226  cvmsss2  35258  cvmliftlem6  35274  cvmliftlem8  35276  mrsubcv  35494  mrsubff  35496  mrsubrn  35497  mrsubccat  35502  elmrsubrn  35504  msubrn  35513  msubff  35514  divcnvlin  35712  faclimlem2  35723  faclim  35725  faclim2  35727  knoppcnlem5  36479  knoppcnlem8  36482  knoppcnlem10  36484  knoppcnlem11  36485  curf  37584  finixpnum  37591  matunitlindflem1  37602  matunitlindflem2  37603  ptrest  37605  poimirlem17  37623  poimirlem20  37626  poimirlem24  37630  poimirlem30  37636  broucube  37640  mblfinlem2  37644  volsupnfl  37651  mbfposadd  37653  itg2addnclem2  37658  itg2gt0cn  37661  ibladdnclem  37662  itgaddnclem1  37664  itgaddnc  37666  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  itgmulc2nclem1  37672  itgmulc2nclem2  37673  itgmulc2nc  37674  itgabsnc  37675  itggt0cn  37676  ftc1cnnc  37678  ftc1anclem1  37679  ftc1anclem2  37680  ftc1anclem3  37681  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  areacirclem4  37697  upixp  37715  totbndbnd  37775  prdsbnd  37779  cntotbnd  37782  rrnequiv  37821  lsatlss  38977  tendoplcl  40763  tendoicl  40778  aks4d1p1p5  42056  aks4d1p9  42069  hashscontpow  42103  sticksstones10  42136  sticksstones17  42144  sticksstones18  42145  unitscyglem1  42176  redvmptabs  42368  fimgmcyc  42520  pwsgprod  42530  evlsval3  42545  evlsvvvallem  42547  evlsvvval  42549  evlsbagval  42552  selvvvval  42571  evlselv  42573  fsuppind  42576  fsuppssind  42579  mhpind  42580  evlsmhpvvval  42581  mhphflem  42582  cmpfiiin  42684  mzpclall  42714  mzpindd  42733  fphpdo  42804  dnnumch3  43035  kelac1  43051  dfac21  43054  cantnfresb  43313  cantnf2  43314  tfsconcatrev  43337  rfovcnvf1od  43993  fsovfd  44001  fsovcnvlem  44002  clsk3nimkb  44029  mnringmulrcld  44223  expgrowth  44330  mptelpm  45118  mapss2  45147  monoord2xrv  45433  expcnfg  45546  clim1fr1  45556  sumnnodd  45585  limsupvaluz2  45693  supcnvlimsup  45695  climliminflimsupd  45756  liminfltlem  45759  cncfmptssg  45826  cncfcompt  45838  cxpcncf2  45854  dvsinax  45868  fperdvper  45874  dvcosax  45881  dvnmptdivc  45893  dvnprodlem2  45902  dvnprodlem3  45903  iblsplit  45921  itgcoscmulx  45924  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  dirkerf  46052  dirkeritg  46057  hoidmvlelem1  46550  hoidmvlelem5  46554  ovnhoilem1  46556  ovnhoilem2  46557  ovnlecvr2  46565  ovncvr2  46566  hoidifhspf  46573  hspmbllem2  46582  opnvonmbllem2  46588  iccvonmbllem  46633  vonioolem1  46635  vonioolem2  46636  vonicclem1  46638  vonicclem2  46639  smfid  46707  cfsetsnfsetf  47007  funcringcsetcALTV2lem3  48135  funcringcsetclem3ALTV  48158  gsumlsscl  48224  ply1mulgsum  48235  lincfsuppcl  48258  linccl  48259  lincsum  48274  lincscmcl  48277  lcoss  48281  lincext1  48299  el0ldep  48311  lincresunit1  48322  lincresunit3  48326  lmod1zr  48338  fdivmptf  48390  refdivmptf  48391  1arymaptf  48490  aacllem  49031  amgmwlem  49032