Theorem fmpttd 5802

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202   ↦ cmpt 4150  ⟶wf 5322

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 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334

This theorem is referenced by:  fmpt3d  5803  pw2f1odclem  7020  ctmlemr  7307  ctssdclemn0  7309  ctssdc  7312  infnninf  7323  nnnninf  7325  ismkvnex  7354  seqf1og  10784  ccatcl  11171  swrdclg  11232  swrdwrdsymbg  11246  fsumf1o  11953  isumss  11954  fisumss  11955  fsumcl2lem  11961  fsumadd  11969  isumclim3  11986  isummulc2  11989  fsummulc2  12011  isumshft  12053  prodfdivap  12110  fprodf1o  12151  prodssdc  12152  fprodssdc  12153  fprodmul  12154  gsumfzz  13580  gsumfzmptfidmadd  13928  gsumfzconst  13930  gsumfzmhm2  13933  srglmhm  14009  srgrmhm  14010  ringlghm  14077  ringrghm  14078  gsumfzfsumlemm  14604  expghmap  14624  fczpsrbag  14688  mplsubgfilemm  14715  tgrest  14896  resttopon  14898  rest0  14906  cnpfval  14922  txcnp  14998  uptx  15001  cnmpt11  15010  bdxmet  15228  cncfmptc  15323  cncfmptid  15324  cdivcncfap  15331  mulcncf  15335  maxcncf  15342  mincncf  15343  ivthreinc  15372  hovercncf  15373  limcmpted  15390  dvfgg  15415  dvcnp2cntop  15426  dvmulxxbr  15429  dvcjbr  15435  dvexp  15438  dvrecap  15440  dvmptclx  15445  dvmptaddx  15446  dvmptmulx  15447  dvmptcjx  15451  dvef  15454  elply2  15462  plyf  15464  elplyd  15468  dvply2g  15493  lgseisenlem3  15804  lgseisenlem4  15805  incistruhgr  15944  2omap  16615  pw1map  16617  subctctexmid  16622  nninffeq  16643  iswomni0  16676  dceqnconst  16685  dcapnconst  16686  gfsumsn  16706