Theorem fmpttd 5837

Description: Version of fmptd 5836 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 5836	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

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

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 4233  ax-pow 4292  ax-pr 4327

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 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-fv 5365

This theorem is referenced by:  fmpt3d  5838  pw2f1odclem  7100  mapxpen  7114  2omap  7282  ctmlemr  7412  ctssdclemn0  7414  ctssdc  7417  infnninf  7428  nnnninf  7430  ismkvnex  7459  seqf1og  10910  ccatcl  11309  swrdclg  11370  swrdwrdsymbg  11384  fsumf1o  12104  isumss  12105  fisumss  12106  fsumcl2lem  12112  fsumadd  12120  isumclim3  12137  isummulc2  12140  fsummulc2  12162  isumshft  12204  prodfdivap  12261  fprodf1o  12302  prodssdc  12303  fprodssdc  12304  fprodmul  12305  gsumfzz  13753  gsumfzmptfidmadd  14095  gsumfzconst  14097  gsumfzmhm2  14100  gfsumsn  14110  gfsumz  14112  srglmhm  14239  srgrmhm  14240  ringlghm  14307  ringrghm  14308  gsumfzfsumlemm  14864  expghmap  14884  fczpsrbag  14949  mplsubgfilemm  14982  tgrest  15163  resttopon  15165  rest0  15173  cnpfval  15189  txcnp  15265  uptx  15268  cnmpt11  15277  bdxmet  15495  cncfmptc  15590  cncfmptid  15591  cdivcncfap  15598  mulcncf  15602  maxcncf  15609  mincncf  15610  ivthreinc  15639  hovercncf  15640  limcmpted  15657  dvfgg  15682  dvcnp2cntop  15693  dvmulxxbr  15696  dvcjbr  15702  dvexp  15705  dvrecap  15707  dvmptclx  15712  dvmptaddx  15713  dvmptmulx  15714  dvmptcjx  15718  dvef  15721  elply2  15729  plyf  15731  elplyd  15735  dvply2g  15760  lgseisenlem3  16074  lgseisenlem4  16075  incistruhgr  16214  pw1map  16908  subctctexmid  16913  nninffeq  16937  iswomni0  16975  dceqnconst  16985  dcapnconst  16986