Theorem fmpttd 5742

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177   ↦ cmpt 4109  ⟶wf 5272

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-pr 4257

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-sbc 3000  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-br 4048  df-opab 4110  df-mpt 4111  df-id 4344  df-xp 4685  df-rel 4686  df-cnv 4687  df-co 4688  df-dm 4689  df-rn 4690  df-res 4691  df-ima 4692  df-iota 5237  df-fun 5278  df-fn 5279  df-f 5280  df-fv 5284

This theorem is referenced by:  fmpt3d  5743  pw2f1odclem  6938  ctmlemr  7217  ctssdclemn0  7219  ctssdc  7222  infnninf  7233  nnnninf  7235  ismkvnex  7264  seqf1og  10673  ccatcl  11057  swrdclg  11111  swrdwrdsymbg  11125  fsumf1o  11745  isumss  11746  fisumss  11747  fsumcl2lem  11753  fsumadd  11761  isumclim3  11778  isummulc2  11781  fsummulc2  11803  isumshft  11845  prodfdivap  11902  fprodf1o  11943  prodssdc  11944  fprodssdc  11945  fprodmul  11946  gsumfzz  13371  gsumfzmptfidmadd  13719  gsumfzconst  13721  gsumfzmhm2  13724  srglmhm  13799  srgrmhm  13800  ringlghm  13867  ringrghm  13868  gsumfzfsumlemm  14393  expghmap  14413  fczpsrbag  14477  mplsubgfilemm  14504  tgrest  14685  resttopon  14687  rest0  14695  cnpfval  14711  txcnp  14787  uptx  14790  cnmpt11  14799  bdxmet  15017  cncfmptc  15112  cncfmptid  15113  cdivcncfap  15120  mulcncf  15124  maxcncf  15131  mincncf  15132  ivthreinc  15161  hovercncf  15162  limcmpted  15179  dvfgg  15204  dvcnp2cntop  15215  dvmulxxbr  15218  dvcjbr  15224  dvexp  15227  dvrecap  15229  dvmptclx  15234  dvmptaddx  15235  dvmptmulx  15236  dvmptcjx  15240  dvef  15243  elply2  15251  plyf  15253  elplyd  15257  dvply2g  15282  lgseisenlem3  15593  lgseisenlem4  15594  incistruhgr  15730  2omap  16006  subctctexmid  16011  nninffeq  16031  iswomni0  16064  dceqnconst  16073  dcapnconst  16074