Theorem fmpttd 5834

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205   ↦ cmpt 4173  ⟶wf 5350

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-sbc 3045  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-mpt 4175  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-res 4763  df-ima 4764  df-iota 5314  df-fun 5356  df-fn 5357  df-f 5358  df-fv 5362

This theorem is referenced by:  fmpt3d  5835  pw2f1odclem  7089  mapxpen  7103  2omap  7271  ctmlemr  7401  ctssdclemn0  7403  ctssdc  7406  infnninf  7417  nnnninf  7419  ismkvnex  7448  seqf1og  10890  ccatcl  11289  swrdclg  11350  swrdwrdsymbg  11364  fsumf1o  12084  isumss  12085  fisumss  12086  fsumcl2lem  12092  fsumadd  12100  isumclim3  12117  isummulc2  12120  fsummulc2  12142  isumshft  12184  prodfdivap  12241  fprodf1o  12282  prodssdc  12283  fprodssdc  12284  fprodmul  12285  gsumfzz  13729  gsumfzmptfidmadd  14077  gsumfzconst  14079  gsumfzmhm2  14082  srglmhm  14158  srgrmhm  14159  ringlghm  14226  ringrghm  14227  gsumfzfsumlemm  14784  expghmap  14804  fczpsrbag  14869  mplsubgfilemm  14902  tgrest  15083  resttopon  15085  rest0  15093  cnpfval  15109  txcnp  15185  uptx  15188  cnmpt11  15197  bdxmet  15415  cncfmptc  15510  cncfmptid  15511  cdivcncfap  15518  mulcncf  15522  maxcncf  15529  mincncf  15530  ivthreinc  15559  hovercncf  15560  limcmpted  15577  dvfgg  15602  dvcnp2cntop  15613  dvmulxxbr  15616  dvcjbr  15622  dvexp  15625  dvrecap  15627  dvmptclx  15632  dvmptaddx  15633  dvmptmulx  15634  dvmptcjx  15638  dvef  15641  elply2  15649  plyf  15651  elplyd  15655  dvply2g  15680  lgseisenlem3  15994  lgseisenlem4  15995  incistruhgr  16134  pw1map  16818  subctctexmid  16823  nninffeq  16847  iswomni0  16885  dceqnconst  16895  dcapnconst  16896  gfsumsn  16916  gfsumz  16918