Theorem fmpttd 7135

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ↦ cmpt 5225  ⟶wf 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565

This theorem is referenced by:  fmpt3d  7136  fliftrel  7328  fsetfocdm  8901  pw2f1olem  9116  mapxpen  9183  fsuppssov1  9424  fsuppmptif  9439  wdom2d  9620  cantnflem1d  9728  cantnflem1  9729  ac5num  10076  acni2  10086  infpwfien  10102  fin23lem39  10390  fin1a2lem12  10451  canthp1lem2  10693  wuncval2  10787  gruf  10851  monoord2  14074  seqf1o  14084  ccatcl  14612  swrdcl  14683  swrdwrdsymb  14700  revcl  14799  revlen  14800  ello1mpt  15557  lo1o12  15569  lo1eq  15604  rlimeq  15605  climmpt2  15609  climrecl  15619  climge0  15620  o1compt  15623  rlimcn1b  15625  rlimdiv  15682  isercoll2  15705  caurcvg2  15714  fsumf1o  15759  sumss  15760  fsumss  15761  fsumcl2lem  15767  fsumadd  15776  isumclim3  15795  isummulc2  15798  fsummulc2  15820  fsumrelem  15843  climfsum  15856  isumshft  15875  divcnv  15889  prodfdiv  15932  fprodf1o  15982  prodss  15983  fprodss  15984  fprodser  15985  fprodcl2lem  15986  fprodmul  15996  fproddiv  15997  fprodn0  16015  iprodclim3  16036  fprodefsum  16131  iserodd  16873  prmreclem2  16955  vdwapf  17010  vdwlem4  17022  ramcl  17067  prmodvdslcmf  17085  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  mrcflem  17649  mreacs  17701  acsfn  17702  hofcllem  18303  hofcl  18304  yonedalem3a  18319  yonedalem4c  18322  yonedainv  18326  prdspjmhm  18842  pwsco1mhm  18845  pwsco2mhm  18846  gsumz  18849  gsumwspan  18859  odf1o1  19590  odf1o2  19591  sylow2blem1  19638  mulgmhm  19845  mulgghm  19846  iscyggen2  19899  cyggenod  19902  iscyg3  19904  gsumzsplit  19945  gsumsplit2  19947  gsumconst  19952  gsummptshft  19954  gsummhm2  19957  gsummptmhm  19958  gsummptf1o  19981  gsum2dlem1  19988  gsum2dlem2  19989  gsum2d  19990  prdsgsum  19999  dprdfeq0  20042  dprdlub  20046  dprdz  20050  dprd2dlem1  20061  dprd2da  20062  srglmhm  20218  srgrmhm  20219  ringlghm  20309  ringrghm  20310  gsumdixp  20316  pwspjmhmmgpd  20325  lmodvsghm  20921  gsumfsum  21452  regsumfsum  21453  expmhm  21454  expghm  21486  evpmodpmf1o  21614  frlmgsum  21792  frlmsplit2  21793  frlmphl  21801  uvcff  21811  uvcresum  21813  snifpsrbag  21940  psrass1lem  21952  rhmpsrlem1  21960  rhmpsrlem2  21961  psrmulcllem  21965  psrlidm  21982  psrridm  21983  psrcom  21988  resspsrmul  21996  mvrf  22005  mplmon  22053  mplmonmul  22054  mplcoe1  22055  mplcoe5lem  22057  mplcoe5  22058  mplbas2  22060  psrbagsn  22087  evlslem4  22100  evlslem2  22103  evlslem3  22104  evlslem6  22105  evlslem1  22106  evlsval2  22111  psdcl  22165  psdmplcl  22166  psdmul  22170  psropprmul  22239  coe1mul2  22272  coe1tmmul2  22279  coe1tmmul  22280  ply1coe  22302  gsumsmonply1  22311  gsummoncoe1  22312  mamulid  22447  mamurid  22448  mdetunilem9  22626  mdetuni0  22627  mdetmul  22629  smadiadetlem3lem1  22672  m2cpmfo  22762  pmatcollpw1  22782  pmatcollpw3lem  22789  pmatcollpw3fi1lem2  22793  pm2mpcl  22803  mply1topmatcl  22811  mp2pm2mplem2  22813  mp2pm2mp  22817  pm2mpmhmlem2  22825  cayhamlem4  22894  pptbas  23015  tgrest  23167  resttopon  23169  rest0  23177  restfpw  23187  ordtbaslem  23196  ordtuni  23198  ordtrest  23210  cnpfval  23242  pnrmopn  23351  cncmp  23400  discmp  23406  1stcfb  23453  2ndcomap  23466  dis2ndc  23468  comppfsc  23540  kgencmp  23553  ptpjpre1  23579  ptpjcn  23619  ptcldmpt  23622  ptclsg  23623  dfac14  23626  xkoccn  23627  txcnp  23628  ptcnp  23630  uptx  23633  ptcn  23635  ptrescn  23647  xkoptsub  23662  xkoco1cn  23665  xkoco2cn  23666  cnmpt11  23671  pt1hmeo  23814  fbasrn  23892  trfilss  23897  trfg  23899  rnelfmlem  23960  flfcnp2  24015  fclscmpi  24037  alexsublem  24052  ptcmplem3  24062  symgtgp  24114  subgntr  24115  opnsubg  24116  clsnsg  24118  tgpconncomp  24121  eltsms  24141  haustsms  24144  tsmscls  24146  tsms0  24150  tsmsmhm  24154  tgptsmscls  24158  tsmssplit  24160  tsmsxplem1  24161  tsmsxplem2  24162  prdsdsf  24377  prdsxmetlem  24378  imasdsf1olem  24383  prdsbl  24504  stdbdxmet  24528  met1stc  24534  xrge0gsumle  24855  xrge0tsms  24856  cncfmpt2ss  24942  cnmptre  24954  evth  24991  evth2  24992  tcphcph  25271  rrxmval  25439  minveclem1  25458  minveclem3b  25462  iunmbl  25588  uniioombllem3  25620  ismbfcn2  25673  mbfeqalem1  25676  mbfeqalem2  25677  mbfss  25681  mbfmulc2re  25683  mbfneg  25685  mbfpos  25686  mbfposr  25687  mbfposb  25688  mbfadd  25696  mbfmulc2  25698  mbfsup  25699  mbfinf  25700  mbflimsup  25701  mbflimlem  25702  mbflim  25703  itg1climres  25749  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1flimlem  25757  mbfi1flim  25758  mbfmullem2  25759  mbfmul  25761  itg2const2  25776  itg2seq  25777  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  itg2cn  25798  iblss  25840  itgitg1  25844  itgle  25845  itgeqa  25849  itgss3  25850  ibladdlem  25855  itgaddlem1  25858  iblabslem  25863  iblabs  25864  iblabsr  25865  iblmulc2  25866  itgmulc2lem1  25867  bddmulibl  25874  bddiblnc  25877  itggt0  25879  itgcn  25880  ellimc2  25912  limcmpt  25918  limcres  25921  limccnp  25926  limccnp2  25927  limcco  25928  perfdvf  25938  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcjbr  25987  dvexp  25991  dvrec  25993  dvmptres3  25994  dvmptadd  25998  dvmptmul  25999  dvmptres2  26000  dvmptcmul  26002  dvmptcj  26006  dvmptntr  26009  dvmptco  26010  dvcnvlem  26014  dvef  26018  dvferm1  26023  dvferm2  26025  rolle  26028  dvlipcn  26033  dvle  26046  dvivth  26049  lhop1lem  26052  lhop1  26053  lhop2  26054  lhop  26055  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvmptrecl  26064  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubstlem  26089  itgpowd  26091  tdeglem4  26099  coe1mul3  26138  elply2  26235  plyf  26237  elplyd  26241  plypf1  26251  coeeq2  26281  coemullem  26289  coe1termlem  26297  dvply2g  26326  dvply2gOLD  26327  elqaalem2  26362  taylfvallem  26399  taylf  26402  tayl0  26403  taylpfval  26406  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmcau  26438  ulmss  26440  ulmdvlem3  26445  mtest  26447  mtestbdd  26448  itgulm2  26452  dvradcnv  26464  pserulm  26465  pserdvlem2  26472  abelthlem9  26484  pige3ALT  26562  logtayl  26702  logccv  26705  loglesqrt  26804  leibpi  26985  rlimcnp  27008  rlimcnp2  27009  xrlimcnp  27011  efrlim  27012  efrlimOLD  27013  dfef2  27014  o1cxp  27018  cxp2lim  27020  amgmlem  27033  lgamgulmlem2  27073  lgamgulmlem6  27077  lgamcvg2  27098  regamcl  27104  relgamcl  27105  basellem2  27125  basellem3  27126  sqff1o  27225  fsumvma  27257  dchrelbasd  27283  lgseisenlem3  27421  lgseisenlem4  27422  chpo1ub  27524  dchrisum0lem2a  27561  logsqvma2  27587  pnt2  27657  pnt  27658  incistruhgr  29096  minvecolem1  30893  hoaddcl  31777  homulcl  31778  cofmpt2  32644  mptiffisupp  32702  fpwrelmap  32744  gsummpt2d  33052  gsummptfsf1o  33057  gsumfs2d  33058  gsumzrsum  33062  xrge0tsmsd  33065  gsumwrd2dccat  33070  gsumvsca1  33232  gsumvsca2  33233  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspn  33250  elrgspnsubrunlem2  33252  elrspunidl  33456  elrspunsn  33457  evl1deg2  33602  fedgmullem1  33680  fedgmullem2  33681  evls1fldgencl  33720  fldextrspunlsplem  33723  fldextrspunlsp  33724  ordtrestNEW  33920  esumf1o  34051  esumadd  34058  esumcst  34064  esumpfinval  34076  esumpcvgval  34079  esumcvg  34087  esumsup  34090  measinb  34222  measdivcst  34225  sitgclg  34344  dstfrvclim1  34480  gsumncl  34555  gsumnunsn  34556  fdvneggt  34615  fdvnegge  34617  itgexpif  34621  logdivsqrle  34665  indispconn  35239  cvxpconn  35247  cvmsss2  35279  cvmliftlem6  35295  cvmliftlem8  35297  mrsubcv  35515  mrsubff  35517  mrsubrn  35518  mrsubccat  35523  elmrsubrn  35525  msubrn  35534  msubff  35535  divcnvlin  35733  faclimlem2  35744  faclim  35746  faclim2  35748  knoppcnlem5  36498  knoppcnlem8  36501  knoppcnlem10  36503  knoppcnlem11  36504  curf  37605  finixpnum  37612  matunitlindflem1  37623  matunitlindflem2  37624  ptrest  37626  poimirlem17  37644  poimirlem20  37647  poimirlem24  37651  poimirlem30  37657  broucube  37661  mblfinlem2  37665  volsupnfl  37672  mbfposadd  37674  itg2addnclem2  37679  itg2gt0cn  37682  ibladdnclem  37683  itgaddnclem1  37685  itgaddnc  37687  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  itgmulc2nclem1  37693  itgmulc2nclem2  37694  itgmulc2nc  37695  itgabsnc  37696  itggt0cn  37697  ftc1cnnc  37699  ftc1anclem1  37700  ftc1anclem2  37701  ftc1anclem3  37702  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  areacirclem4  37718  upixp  37736  totbndbnd  37796  prdsbnd  37800  cntotbnd  37803  rrnequiv  37842  lsatlss  38997  tendoplcl  40783  tendoicl  40798  aks4d1p1p5  42076  aks4d1p9  42089  hashscontpow  42123  sticksstones10  42156  sticksstones17  42164  sticksstones18  42165  unitscyglem1  42196  redvmptabs  42390  fimgmcyc  42544  pwsgprod  42554  evlsval3  42569  evlsvvvallem  42571  evlsvvval  42573  evlsbagval  42576  selvvvval  42595  evlselv  42597  fsuppind  42600  fsuppssind  42603  mhpind  42604  evlsmhpvvval  42605  mhphflem  42606  cmpfiiin  42708  mzpclall  42738  mzpindd  42757  fphpdo  42828  dnnumch3  43059  kelac1  43075  dfac21  43078  cantnfresb  43337  cantnf2  43338  tfsconcatrev  43361  rfovcnvf1od  44017  fsovfd  44025  fsovcnvlem  44026  clsk3nimkb  44053  mnringmulrcld  44247  expgrowth  44354  mptelpm  45181  mapss2  45210  monoord2xrv  45494  expcnfg  45606  clim1fr1  45616  sumnnodd  45645  limsupvaluz2  45753  supcnvlimsup  45755  climliminflimsupd  45816  liminfltlem  45819  cncfmptssg  45886  cncfcompt  45898  cxpcncf2  45914  dvsinax  45928  fperdvper  45934  dvcosax  45941  dvnmptdivc  45953  dvnprodlem2  45962  dvnprodlem3  45963  iblsplit  45981  itgcoscmulx  45984  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  dirkerf  46112  dirkeritg  46117  hoidmvlelem1  46610  hoidmvlelem5  46614  ovnhoilem1  46616  ovnhoilem2  46617  ovnlecvr2  46625  ovncvr2  46626  hoidifhspf  46633  hspmbllem2  46642  opnvonmbllem2  46648  iccvonmbllem  46693  vonioolem1  46695  vonioolem2  46696  vonicclem1  46698  vonicclem2  46699  smfid  46767  cfsetsnfsetf  47070  funcringcsetcALTV2lem3  48208  funcringcsetclem3ALTV  48231  gsumlsscl  48296  ply1mulgsum  48307  lincfsuppcl  48330  linccl  48331  lincsum  48346  lincscmcl  48349  lcoss  48353  lincext1  48371  el0ldep  48383  lincresunit1  48394  lincresunit3  48398  lmod1zr  48410  fdivmptf  48462  refdivmptf  48463  1arymaptf  48562  aacllem  49320  amgmwlem  49321