Theorem fmpttd 7057

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ↦ cmpt 5176  ⟶wf 6485

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-fun 6491  df-fn 6492  df-f 6493

This theorem is referenced by:  fmpt3d  7058  fliftrel  7251  fsetfocdm  8794  pw2f1olem  9004  mapxpen  9066  fsuppssov1  9278  fsuppmptif  9293  wdom2d  9476  cantnflem1d  9588  cantnflem1  9589  ac5num  9937  acni2  9947  infpwfien  9963  fin23lem39  10251  fin1a2lem12  10312  canthp1lem2  10554  wuncval2  10648  gruf  10712  monoord2  13950  seqf1o  13960  ccatcl  14491  swrdcl  14563  swrdwrdsymb  14580  revcl  14678  revlen  14679  ello1mpt  15438  lo1o12  15450  lo1eq  15485  rlimeq  15486  climmpt2  15490  climrecl  15500  climge0  15501  o1compt  15504  rlimcn1b  15506  rlimdiv  15563  isercoll2  15586  caurcvg2  15595  fsumf1o  15640  sumss  15641  fsumss  15642  fsumcl2lem  15648  fsumadd  15657  isumclim3  15676  isummulc2  15679  fsummulc2  15701  fsumrelem  15724  climfsum  15737  isumshft  15756  divcnv  15770  prodfdiv  15813  fprodf1o  15863  prodss  15864  fprodss  15865  fprodser  15866  fprodcl2lem  15867  fprodmul  15877  fproddiv  15878  fprodn0  15896  iprodclim3  15917  fprodefsum  16012  iserodd  16757  prmreclem2  16839  vdwapf  16894  vdwlem4  16906  ramcl  16951  prmodvdslcmf  16969  prdsplusg  17372  prdsmulr  17373  prdsvsca  17374  mrcflem  17522  mreacs  17574  acsfn  17575  hofcllem  18174  hofcl  18175  yonedalem3a  18190  yonedalem4c  18193  yonedainv  18197  prdspjmhm  18747  pwsco1mhm  18750  pwsco2mhm  18751  gsumz  18754  gsumwspan  18764  odf1o1  19494  odf1o2  19495  sylow2blem1  19542  mulgmhm  19749  mulgghm  19750  iscyggen2  19803  cyggenod  19806  iscyg3  19808  gsumzsplit  19849  gsumsplit2  19851  gsumconst  19856  gsummptshft  19858  gsummhm2  19861  gsummptmhm  19862  gsummptf1o  19885  gsum2dlem1  19892  gsum2dlem2  19893  gsum2d  19894  prdsgsum  19903  dprdfeq0  19946  dprdlub  19950  dprdz  19954  dprd2dlem1  19965  dprd2da  19966  srglmhm  20149  srgrmhm  20150  ringlghm  20240  ringrghm  20241  gsumdixp  20247  pwspjmhmmgpd  20256  lmodvsghm  20866  gsumfsum  21381  regsumfsum  21382  expmhm  21383  expghm  21422  evpmodpmf1o  21543  frlmgsum  21719  frlmsplit2  21720  frlmphl  21728  uvcff  21738  uvcresum  21740  snifpsrbag  21867  psrass1lem  21879  rhmpsrlem1  21887  rhmpsrlem2  21888  psrmulcllem  21892  psrlidm  21909  psrridm  21910  psrcom  21915  resspsrmul  21923  mvrf  21932  mplmon  21980  mplmonmul  21981  mplcoe1  21982  mplcoe5lem  21984  mplcoe5  21985  mplbas2  21987  psrbagsn  22008  evlslem4  22021  evlslem2  22024  evlslem3  22025  evlslem6  22026  evlslem1  22027  evlsval2  22032  psdcl  22086  psdmplcl  22087  psdmul  22091  psropprmul  22160  coe1mul2  22193  coe1tmmul2  22200  coe1tmmul  22201  ply1coe  22223  gsumsmonply1  22232  gsummoncoe1  22233  mamulid  22366  mamurid  22367  mdetunilem9  22545  mdetuni0  22546  mdetmul  22548  smadiadetlem3lem1  22591  m2cpmfo  22681  pmatcollpw1  22701  pmatcollpw3lem  22708  pmatcollpw3fi1lem2  22712  pm2mpcl  22722  mply1topmatcl  22730  mp2pm2mplem2  22732  mp2pm2mp  22736  pm2mpmhmlem2  22744  cayhamlem4  22813  pptbas  22933  tgrest  23084  resttopon  23086  rest0  23094  restfpw  23104  ordtbaslem  23113  ordtuni  23115  ordtrest  23127  cnpfval  23159  pnrmopn  23268  cncmp  23317  discmp  23323  1stcfb  23370  2ndcomap  23383  dis2ndc  23385  comppfsc  23457  kgencmp  23470  ptpjpre1  23496  ptpjcn  23536  ptcldmpt  23539  ptclsg  23540  dfac14  23543  xkoccn  23544  txcnp  23545  ptcnp  23547  uptx  23550  ptcn  23552  ptrescn  23564  xkoptsub  23579  xkoco1cn  23582  xkoco2cn  23583  cnmpt11  23588  pt1hmeo  23731  fbasrn  23809  trfilss  23814  trfg  23816  rnelfmlem  23877  flfcnp2  23932  fclscmpi  23954  alexsublem  23969  ptcmplem3  23979  symgtgp  24031  subgntr  24032  opnsubg  24033  clsnsg  24035  tgpconncomp  24038  eltsms  24058  haustsms  24061  tsmscls  24063  tsms0  24067  tsmsmhm  24071  tgptsmscls  24075  tsmssplit  24077  tsmsxplem1  24078  tsmsxplem2  24079  prdsdsf  24292  prdsxmetlem  24293  imasdsf1olem  24298  prdsbl  24416  stdbdxmet  24440  met1stc  24446  xrge0gsumle  24759  xrge0tsms  24760  cncfmpt2ss  24846  cnmptre  24858  evth  24895  evth2  24896  tcphcph  25174  rrxmval  25342  minveclem1  25361  minveclem3b  25365  iunmbl  25491  uniioombllem3  25523  ismbfcn2  25576  mbfeqalem1  25579  mbfeqalem2  25580  mbfss  25584  mbfmulc2re  25586  mbfneg  25588  mbfpos  25589  mbfposr  25590  mbfposb  25591  mbfadd  25599  mbfmulc2  25601  mbfsup  25602  mbfinf  25603  mbflimsup  25604  mbflimlem  25605  mbflim  25606  itg1climres  25652  mbfi1fseqlem3  25655  mbfi1fseqlem4  25656  mbfi1flimlem  25660  mbfi1flim  25661  mbfmullem2  25662  mbfmul  25664  itg2const2  25679  itg2seq  25680  itg2monolem1  25688  itg2monolem2  25689  itg2monolem3  25690  itg2mono  25691  itg2gt0  25698  itg2cnlem1  25699  itg2cnlem2  25700  itg2cn  25701  iblss  25743  itgitg1  25747  itgle  25748  itgeqa  25752  itgss3  25753  ibladdlem  25758  itgaddlem1  25761  iblabslem  25766  iblabs  25767  iblabsr  25768  iblmulc2  25769  itgmulc2lem1  25770  bddmulibl  25777  bddiblnc  25780  itggt0  25782  itgcn  25783  ellimc2  25815  limcmpt  25821  limcres  25824  limccnp  25829  limccnp2  25830  limcco  25831  perfdvf  25841  dvcnp2  25858  dvcnp2OLD  25859  dvaddbr  25877  dvmulbr  25878  dvmulbrOLD  25879  dvcjbr  25890  dvexp  25894  dvrec  25896  dvmptres3  25897  dvmptadd  25901  dvmptmul  25902  dvmptres2  25903  dvmptcmul  25905  dvmptcj  25909  dvmptntr  25912  dvmptco  25913  dvcnvlem  25917  dvef  25921  dvferm1  25926  dvferm2  25928  rolle  25931  dvlipcn  25936  dvle  25949  dvivth  25952  lhop1lem  25955  lhop1  25956  lhop2  25957  lhop  25958  dvfsumle  25963  dvfsumleOLD  25964  dvfsumge  25965  dvmptrecl  25967  dvfsumlem2  25970  dvfsumlem2OLD  25971  itgsubstlem  25992  itgpowd  25994  tdeglem4  26002  coe1mul3  26041  elply2  26138  plyf  26140  elplyd  26144  plypf1  26154  coeeq2  26184  coemullem  26192  coe1termlem  26200  dvply2g  26229  dvply2gOLD  26230  elqaalem2  26265  taylfvallem  26302  taylf  26305  tayl0  26306  taylpfval  26309  taylthlem1  26318  taylthlem2  26319  taylthlem2OLD  26320  ulmcau  26341  ulmss  26343  ulmdvlem3  26348  mtest  26350  mtestbdd  26351  itgulm2  26355  dvradcnv  26367  pserulm  26368  pserdvlem2  26375  abelthlem9  26387  pige3ALT  26466  logtayl  26606  logccv  26609  loglesqrt  26708  leibpi  26889  rlimcnp  26912  rlimcnp2  26913  xrlimcnp  26915  efrlim  26916  efrlimOLD  26917  dfef2  26918  o1cxp  26922  cxp2lim  26924  amgmlem  26937  lgamgulmlem2  26977  lgamgulmlem6  26981  lgamcvg2  27002  regamcl  27008  relgamcl  27009  basellem2  27029  basellem3  27030  sqff1o  27129  fsumvma  27161  dchrelbasd  27187  lgseisenlem3  27325  lgseisenlem4  27326  chpo1ub  27428  dchrisum0lem2a  27465  logsqvma2  27491  pnt2  27561  pnt  27562  incistruhgr  29068  minvecolem1  30865  hoaddcl  31749  homulcl  31750  cofmpt2  32627  mptiffisupp  32685  fpwrelmap  32727  gsummpt2d  33040  gsummptfsf1o  33045  gsumfs2d  33046  gsumzrsum  33050  xrge0tsmsd  33053  gsumwrd2dccat  33058  gsumvsca1  33206  gsumvsca2  33207  elrgspnlem1  33220  elrgspnlem2  33221  elrgspnlem3  33222  elrgspnlem4  33223  elrgspn  33224  elrgspnsubrunlem2  33226  elrspunidl  33404  elrspunsn  33405  ressply1evls1  33539  evl1deg2  33551  mplvrpmga  33586  fedgmullem1  33653  fedgmullem2  33654  evls1fldgencl  33694  fldextrspunlsplem  33697  fldextrspunlsp  33698  extdgfialglem2  33717  ordtrestNEW  33945  esumf1o  34074  esumadd  34081  esumcst  34087  esumpfinval  34099  esumpcvgval  34102  esumcvg  34110  esumsup  34113  measinb  34245  measdivcst  34248  sitgclg  34366  dstfrvclim1  34502  gsumncl  34564  gsumnunsn  34565  fdvneggt  34624  fdvnegge  34626  itgexpif  34630  logdivsqrle  34674  indispconn  35289  cvxpconn  35297  cvmsss2  35329  cvmliftlem6  35345  cvmliftlem8  35347  mrsubcv  35565  mrsubff  35567  mrsubrn  35568  mrsubccat  35573  elmrsubrn  35575  msubrn  35584  msubff  35585  divcnvlin  35788  faclimlem2  35799  faclim  35801  faclim2  35803  knoppcnlem5  36552  knoppcnlem8  36555  knoppcnlem10  36557  knoppcnlem11  36558  curf  37648  finixpnum  37655  matunitlindflem1  37666  matunitlindflem2  37667  ptrest  37669  poimirlem17  37687  poimirlem20  37690  poimirlem24  37694  poimirlem30  37700  broucube  37704  mblfinlem2  37708  volsupnfl  37715  mbfposadd  37717  itg2addnclem2  37722  itg2gt0cn  37725  ibladdnclem  37726  itgaddnclem1  37728  itgaddnc  37730  iblabsnclem  37733  iblabsnc  37734  iblmulc2nc  37735  itgmulc2nclem1  37736  itgmulc2nclem2  37737  itgmulc2nc  37738  itgabsnc  37739  itggt0cn  37740  ftc1cnnc  37742  ftc1anclem1  37743  ftc1anclem2  37744  ftc1anclem3  37745  ftc1anclem4  37746  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  areacirclem4  37761  upixp  37779  totbndbnd  37839  prdsbnd  37843  cntotbnd  37846  rrnequiv  37885  lsatlss  39105  tendoplcl  40890  tendoicl  40905  aks4d1p1p5  42178  aks4d1p9  42191  hashscontpow  42225  sticksstones10  42258  sticksstones17  42266  sticksstones18  42267  unitscyglem1  42298  redvmptabs  42468  fimgmcyc  42642  pwsgprod  42652  evlsval3  42667  evlsvvvallem  42669  evlsvvval  42671  evlsbagval  42674  selvvvval  42693  evlselv  42695  fsuppind  42698  fsuppssind  42701  mhpind  42702  evlsmhpvvval  42703  mhphflem  42704  cmpfiiin  42804  mzpclall  42834  mzpindd  42853  fphpdo  42924  dnnumch3  43154  kelac1  43170  dfac21  43173  cantnfresb  43431  cantnf2  43432  tfsconcatrev  43455  rfovcnvf1od  44111  fsovfd  44119  fsovcnvlem  44120  clsk3nimkb  44147  mnringmulrcld  44335  expgrowth  44442  mptelpm  45287  mapss2  45316  monoord2xrv  45595  expcnfg  45705  clim1fr1  45715  sumnnodd  45744  limsupvaluz2  45850  supcnvlimsup  45852  climliminflimsupd  45913  liminfltlem  45916  cncfmptssg  45983  cncfcompt  45995  cxpcncf2  46011  dvsinax  46025  fperdvper  46031  dvcosax  46038  dvnmptdivc  46050  dvnprodlem2  46059  dvnprodlem3  46060  iblsplit  46078  itgcoscmulx  46081  itgiccshift  46092  itgperiod  46093  itgsbtaddcnst  46094  dirkerf  46209  dirkeritg  46214  hoidmvlelem1  46707  hoidmvlelem5  46711  ovnhoilem1  46713  ovnhoilem2  46714  ovnlecvr2  46722  ovncvr2  46723  hoidifhspf  46730  hspmbllem2  46739  opnvonmbllem2  46745  iccvonmbllem  46790  vonioolem1  46792  vonioolem2  46793  vonicclem1  46795  vonicclem2  46796  smfid  46864  cfsetsnfsetf  47172  funcringcsetcALTV2lem3  48406  funcringcsetclem3ALTV  48429  gsumlsscl  48494  ply1mulgsum  48505  lincfsuppcl  48528  linccl  48529  lincsum  48544  lincscmcl  48547  lcoss  48551  lincext1  48569  el0ldep  48581  lincresunit1  48592  lincresunit3  48596  lmod1zr  48608  fdivmptf  48656  refdivmptf  48657  1arymaptf  48756  aacllem  49916  amgmwlem  49917