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  10887  ccatcl  11285  swrdclg  11346  swrdwrdsymbg  11360  fsumf1o  12080  isumss  12081  fisumss  12082  fsumcl2lem  12088  fsumadd  12096  isumclim3  12113  isummulc2  12116  fsummulc2  12138  isumshft  12180  prodfdivap  12237  fprodf1o  12278  prodssdc  12279  fprodssdc  12280  fprodmul  12281  gsumfzz  13725  gsumfzmptfidmadd  14073  gsumfzconst  14075  gsumfzmhm2  14078  srglmhm  14154  srgrmhm  14155  ringlghm  14222  ringrghm  14223  gsumfzfsumlemm  14752  expghmap  14772  fczpsrbag  14837  mplsubgfilemm  14870  tgrest  15051  resttopon  15053  rest0  15061  cnpfval  15077  txcnp  15153  uptx  15156  cnmpt11  15165  bdxmet  15383  cncfmptc  15478  cncfmptid  15479  cdivcncfap  15486  mulcncf  15490  maxcncf  15497  mincncf  15498  ivthreinc  15527  hovercncf  15528  limcmpted  15545  dvfgg  15570  dvcnp2cntop  15581  dvmulxxbr  15584  dvcjbr  15590  dvexp  15593  dvrecap  15595  dvmptclx  15600  dvmptaddx  15601  dvmptmulx  15602  dvmptcjx  15606  dvef  15609  elply2  15617  plyf  15619  elplyd  15623  dvply2g  15648  lgseisenlem3  15962  lgseisenlem4  15963  incistruhgr  16102  pw1map  16786  subctctexmid  16791  nninffeq  16815  iswomni0  16853  dceqnconst  16863  dcapnconst  16864  gfsumsn  16884  gfsumz  16886