Theorem fmpttd 7087

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ↦ cmpt 5188  ⟶wf 6507

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  fmpt3d  7088  fliftrel  7283  fsetfocdm  8834  pw2f1olem  9045  mapxpen  9107  fsuppssov1  9335  fsuppmptif  9350  wdom2d  9533  cantnflem1d  9641  cantnflem1  9642  ac5num  9989  acni2  9999  infpwfien  10015  fin23lem39  10303  fin1a2lem12  10364  canthp1lem2  10606  wuncval2  10700  gruf  10764  monoord2  13998  seqf1o  14008  ccatcl  14539  swrdcl  14610  swrdwrdsymb  14627  revcl  14726  revlen  14727  ello1mpt  15487  lo1o12  15499  lo1eq  15534  rlimeq  15535  climmpt2  15539  climrecl  15549  climge0  15550  o1compt  15553  rlimcn1b  15555  rlimdiv  15612  isercoll2  15635  caurcvg2  15644  fsumf1o  15689  sumss  15690  fsumss  15691  fsumcl2lem  15697  fsumadd  15706  isumclim3  15725  isummulc2  15728  fsummulc2  15750  fsumrelem  15773  climfsum  15786  isumshft  15805  divcnv  15819  prodfdiv  15862  fprodf1o  15912  prodss  15913  fprodss  15914  fprodser  15915  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodn0  15945  iprodclim3  15966  fprodefsum  16061  iserodd  16806  prmreclem2  16888  vdwapf  16943  vdwlem4  16955  ramcl  17000  prmodvdslcmf  17018  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  mrcflem  17567  mreacs  17619  acsfn  17620  hofcllem  18219  hofcl  18220  yonedalem3a  18235  yonedalem4c  18238  yonedainv  18242  prdspjmhm  18756  pwsco1mhm  18759  pwsco2mhm  18760  gsumz  18763  gsumwspan  18773  odf1o1  19502  odf1o2  19503  sylow2blem1  19550  mulgmhm  19757  mulgghm  19758  iscyggen2  19811  cyggenod  19814  iscyg3  19816  gsumzsplit  19857  gsumsplit2  19859  gsumconst  19864  gsummptshft  19866  gsummhm2  19869  gsummptmhm  19870  gsummptf1o  19893  gsum2dlem1  19900  gsum2dlem2  19901  gsum2d  19902  prdsgsum  19911  dprdfeq0  19954  dprdlub  19958  dprdz  19962  dprd2dlem1  19973  dprd2da  19974  srglmhm  20130  srgrmhm  20131  ringlghm  20221  ringrghm  20222  gsumdixp  20228  pwspjmhmmgpd  20237  lmodvsghm  20829  gsumfsum  21351  regsumfsum  21352  expmhm  21353  expghm  21385  evpmodpmf1o  21505  frlmgsum  21681  frlmsplit2  21682  frlmphl  21690  uvcff  21700  uvcresum  21702  snifpsrbag  21829  psrass1lem  21841  rhmpsrlem1  21849  rhmpsrlem2  21850  psrmulcllem  21854  psrlidm  21871  psrridm  21872  psrcom  21877  resspsrmul  21885  mvrf  21894  mplmon  21942  mplmonmul  21943  mplcoe1  21944  mplcoe5lem  21946  mplcoe5  21947  mplbas2  21949  psrbagsn  21970  evlslem4  21983  evlslem2  21986  evlslem3  21987  evlslem6  21988  evlslem1  21989  evlsval2  21994  psdcl  22048  psdmplcl  22049  psdmul  22053  psropprmul  22122  coe1mul2  22155  coe1tmmul2  22162  coe1tmmul  22163  ply1coe  22185  gsumsmonply1  22194  gsummoncoe1  22195  mamulid  22328  mamurid  22329  mdetunilem9  22507  mdetuni0  22508  mdetmul  22510  smadiadetlem3lem1  22553  m2cpmfo  22643  pmatcollpw1  22663  pmatcollpw3lem  22670  pmatcollpw3fi1lem2  22674  pm2mpcl  22684  mply1topmatcl  22692  mp2pm2mplem2  22694  mp2pm2mp  22698  pm2mpmhmlem2  22706  cayhamlem4  22775  pptbas  22895  tgrest  23046  resttopon  23048  rest0  23056  restfpw  23066  ordtbaslem  23075  ordtuni  23077  ordtrest  23089  cnpfval  23121  pnrmopn  23230  cncmp  23279  discmp  23285  1stcfb  23332  2ndcomap  23345  dis2ndc  23347  comppfsc  23419  kgencmp  23432  ptpjpre1  23458  ptpjcn  23498  ptcldmpt  23501  ptclsg  23502  dfac14  23505  xkoccn  23506  txcnp  23507  ptcnp  23509  uptx  23512  ptcn  23514  ptrescn  23526  xkoptsub  23541  xkoco1cn  23544  xkoco2cn  23545  cnmpt11  23550  pt1hmeo  23693  fbasrn  23771  trfilss  23776  trfg  23778  rnelfmlem  23839  flfcnp2  23894  fclscmpi  23916  alexsublem  23931  ptcmplem3  23941  symgtgp  23993  subgntr  23994  opnsubg  23995  clsnsg  23997  tgpconncomp  24000  eltsms  24020  haustsms  24023  tsmscls  24025  tsms0  24029  tsmsmhm  24033  tgptsmscls  24037  tsmssplit  24039  tsmsxplem1  24040  tsmsxplem2  24041  prdsdsf  24255  prdsxmetlem  24256  imasdsf1olem  24261  prdsbl  24379  stdbdxmet  24403  met1stc  24409  xrge0gsumle  24722  xrge0tsms  24723  cncfmpt2ss  24809  cnmptre  24821  evth  24858  evth2  24859  tcphcph  25137  rrxmval  25305  minveclem1  25324  minveclem3b  25328  iunmbl  25454  uniioombllem3  25486  ismbfcn2  25539  mbfeqalem1  25542  mbfeqalem2  25543  mbfss  25547  mbfmulc2re  25549  mbfneg  25551  mbfpos  25552  mbfposr  25553  mbfposb  25554  mbfadd  25562  mbfmulc2  25564  mbfsup  25565  mbfinf  25566  mbflimsup  25567  mbflimlem  25568  mbflim  25569  itg1climres  25615  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1flimlem  25623  mbfi1flim  25624  mbfmullem2  25625  mbfmul  25627  itg2const2  25642  itg2seq  25643  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  itg2cn  25664  iblss  25706  itgitg1  25710  itgle  25711  itgeqa  25715  itgss3  25716  ibladdlem  25721  itgaddlem1  25724  iblabslem  25729  iblabs  25730  iblabsr  25731  iblmulc2  25732  itgmulc2lem1  25733  bddmulibl  25740  bddiblnc  25743  itggt0  25745  itgcn  25746  ellimc2  25778  limcmpt  25784  limcres  25787  limccnp  25792  limccnp2  25793  limcco  25794  perfdvf  25804  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcjbr  25853  dvexp  25857  dvrec  25859  dvmptres3  25860  dvmptadd  25864  dvmptmul  25865  dvmptres2  25866  dvmptcmul  25868  dvmptcj  25872  dvmptntr  25875  dvmptco  25876  dvcnvlem  25880  dvef  25884  dvferm1  25889  dvferm2  25891  rolle  25894  dvlipcn  25899  dvle  25912  dvivth  25915  lhop1lem  25918  lhop1  25919  lhop2  25920  lhop  25921  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvmptrecl  25930  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgsubstlem  25955  itgpowd  25957  tdeglem4  25965  coe1mul3  26004  elply2  26101  plyf  26103  elplyd  26107  plypf1  26117  coeeq2  26147  coemullem  26155  coe1termlem  26163  dvply2g  26192  dvply2gOLD  26193  elqaalem2  26228  taylfvallem  26265  taylf  26268  tayl0  26269  taylpfval  26272  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmcau  26304  ulmss  26306  ulmdvlem3  26311  mtest  26313  mtestbdd  26314  itgulm2  26318  dvradcnv  26330  pserulm  26331  pserdvlem2  26338  abelthlem9  26350  pige3ALT  26429  logtayl  26569  logccv  26572  loglesqrt  26671  leibpi  26852  rlimcnp  26875  rlimcnp2  26876  xrlimcnp  26878  efrlim  26879  efrlimOLD  26880  dfef2  26881  o1cxp  26885  cxp2lim  26887  amgmlem  26900  lgamgulmlem2  26940  lgamgulmlem6  26944  lgamcvg2  26965  regamcl  26971  relgamcl  26972  basellem2  26992  basellem3  26993  sqff1o  27092  fsumvma  27124  dchrelbasd  27150  lgseisenlem3  27288  lgseisenlem4  27289  chpo1ub  27391  dchrisum0lem2a  27428  logsqvma2  27454  pnt2  27524  pnt  27525  incistruhgr  29006  minvecolem1  30803  hoaddcl  31687  homulcl  31688  cofmpt2  32558  mptiffisupp  32616  fpwrelmap  32656  gsummpt2d  32989  gsummptfsf1o  32994  gsumfs2d  32995  gsumzrsum  32999  xrge0tsmsd  33002  gsumwrd2dccat  33007  gsumvsca1  33179  gsumvsca2  33180  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspn  33197  elrgspnsubrunlem2  33199  elrspunidl  33399  elrspunsn  33400  ressply1evls1  33534  evl1deg2  33546  fedgmullem1  33625  fedgmullem2  33626  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  ordtrestNEW  33911  esumf1o  34040  esumadd  34047  esumcst  34053  esumpfinval  34065  esumpcvgval  34068  esumcvg  34076  esumsup  34079  measinb  34211  measdivcst  34214  sitgclg  34333  dstfrvclim1  34469  gsumncl  34531  gsumnunsn  34532  fdvneggt  34591  fdvnegge  34593  itgexpif  34597  logdivsqrle  34641  indispconn  35221  cvxpconn  35229  cvmsss2  35261  cvmliftlem6  35277  cvmliftlem8  35279  mrsubcv  35497  mrsubff  35499  mrsubrn  35500  mrsubccat  35505  elmrsubrn  35507  msubrn  35516  msubff  35517  divcnvlin  35720  faclimlem2  35731  faclim  35733  faclim2  35735  knoppcnlem5  36485  knoppcnlem8  36488  knoppcnlem10  36490  knoppcnlem11  36491  curf  37592  finixpnum  37599  matunitlindflem1  37610  matunitlindflem2  37611  ptrest  37613  poimirlem17  37631  poimirlem20  37634  poimirlem24  37638  poimirlem30  37644  broucube  37648  mblfinlem2  37652  volsupnfl  37659  mbfposadd  37661  itg2addnclem2  37666  itg2gt0cn  37669  ibladdnclem  37670  itgaddnclem1  37672  itgaddnc  37674  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  itgmulc2nclem1  37680  itgmulc2nclem2  37681  itgmulc2nc  37682  itgabsnc  37683  itggt0cn  37684  ftc1cnnc  37686  ftc1anclem1  37687  ftc1anclem2  37688  ftc1anclem3  37689  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirclem4  37705  upixp  37723  totbndbnd  37783  prdsbnd  37787  cntotbnd  37790  rrnequiv  37829  lsatlss  38989  tendoplcl  40775  tendoicl  40790  aks4d1p1p5  42063  aks4d1p9  42076  hashscontpow  42110  sticksstones10  42143  sticksstones17  42151  sticksstones18  42152  unitscyglem1  42183  redvmptabs  42348  fimgmcyc  42522  pwsgprod  42532  evlsval3  42547  evlsvvvallem  42549  evlsvvval  42551  evlsbagval  42554  selvvvval  42573  evlselv  42575  fsuppind  42578  fsuppssind  42581  mhpind  42582  evlsmhpvvval  42583  mhphflem  42584  cmpfiiin  42685  mzpclall  42715  mzpindd  42734  fphpdo  42805  dnnumch3  43036  kelac1  43052  dfac21  43055  cantnfresb  43313  cantnf2  43314  tfsconcatrev  43337  rfovcnvf1od  43993  fsovfd  44001  fsovcnvlem  44002  clsk3nimkb  44029  mnringmulrcld  44217  expgrowth  44324  mptelpm  45170  mapss2  45199  monoord2xrv  45479  expcnfg  45589  clim1fr1  45599  sumnnodd  45628  limsupvaluz2  45736  supcnvlimsup  45738  climliminflimsupd  45799  liminfltlem  45802  cncfmptssg  45869  cncfcompt  45881  cxpcncf2  45897  dvsinax  45911  fperdvper  45917  dvcosax  45924  dvnmptdivc  45936  dvnprodlem2  45945  dvnprodlem3  45946  iblsplit  45964  itgcoscmulx  45967  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  dirkerf  46095  dirkeritg  46100  hoidmvlelem1  46593  hoidmvlelem5  46597  ovnhoilem1  46599  ovnhoilem2  46600  ovnlecvr2  46608  ovncvr2  46609  hoidifhspf  46616  hspmbllem2  46625  opnvonmbllem2  46631  iccvonmbllem  46676  vonioolem1  46678  vonioolem2  46679  vonicclem1  46681  vonicclem2  46682  smfid  46750  cfsetsnfsetf  47059  funcringcsetcALTV2lem3  48280  funcringcsetclem3ALTV  48303  gsumlsscl  48368  ply1mulgsum  48379  lincfsuppcl  48402  linccl  48403  lincsum  48418  lincscmcl  48421  lcoss  48425  lincext1  48443  el0ldep  48455  lincresunit1  48466  lincresunit3  48470  lmod1zr  48482  fdivmptf  48530  refdivmptf  48531  1arymaptf  48630  aacllem  49790  amgmwlem  49791