Theorem fmpttd 5805

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2201   ↦ cmpt 4151  ⟶wf 5324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-rab 2518  df-v 2803  df-sbc 3031  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-opab 4152  df-mpt 4153  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-fv 5336

This theorem is referenced by:  fmpt3d  5806  pw2f1odclem  7025  ctmlemr  7312  ctssdclemn0  7314  ctssdc  7317  infnninf  7328  nnnninf  7330  ismkvnex  7359  seqf1og  10789  ccatcl  11179  swrdclg  11240  swrdwrdsymbg  11254  fsumf1o  11974  isumss  11975  fisumss  11976  fsumcl2lem  11982  fsumadd  11990  isumclim3  12007  isummulc2  12010  fsummulc2  12032  isumshft  12074  prodfdivap  12131  fprodf1o  12172  prodssdc  12173  fprodssdc  12174  fprodmul  12175  gsumfzz  13601  gsumfzmptfidmadd  13949  gsumfzconst  13951  gsumfzmhm2  13954  srglmhm  14030  srgrmhm  14031  ringlghm  14098  ringrghm  14099  gsumfzfsumlemm  14625  expghmap  14645  fczpsrbag  14709  mplsubgfilemm  14741  tgrest  14922  resttopon  14924  rest0  14932  cnpfval  14948  txcnp  15024  uptx  15027  cnmpt11  15036  bdxmet  15254  cncfmptc  15349  cncfmptid  15350  cdivcncfap  15357  mulcncf  15361  maxcncf  15368  mincncf  15369  ivthreinc  15398  hovercncf  15399  limcmpted  15416  dvfgg  15441  dvcnp2cntop  15452  dvmulxxbr  15455  dvcjbr  15461  dvexp  15464  dvrecap  15466  dvmptclx  15471  dvmptaddx  15472  dvmptmulx  15473  dvmptcjx  15477  dvef  15480  elply2  15488  plyf  15490  elplyd  15494  dvply2g  15519  lgseisenlem3  15830  lgseisenlem4  15831  incistruhgr  15970  2omap  16654  pw1map  16656  subctctexmid  16661  nninffeq  16685  iswomni0  16723  dceqnconst  16732  dcapnconst  16733  gfsumsn  16753