Theorem fmpttd 5866

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209   ↦ cmpt 4193  ⟶wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388

This theorem is used by:  fmpt3d  5867  pw2f1odclem  7139  mapxpen  7153  2omap  7325  ctmlemr  7455  ctssdclemn0  7457  ctssdc  7460  infnninf  7471  nnnninf  7473  ismkvnex  7502  seqf1og  10980  ccatcl  11384  swrdclg  11445  swrdwrdsymbg  11459  fsumf1o  12183  isumss  12184  fisumss  12185  fsumcl2lem  12191  fsumadd  12199  isumclim3  12216  isummulc2  12219  fsummulc2  12241  isumshft  12283  prodfdivap  12340  fprodf1o  12381  prodssdc  12382  fprodssdc  12383  fprodmul  12384  gzsumconst  14234  gzsummhm2  14237  gsumsncmn  14247  gsumzfi  14249  gsummptfidmadd  14252  gsummptfidmsplit  14255  gsummhm2fi  14266  gsumconstcmn  14267  gsum2dfilem1  14272  gsum2dfilem2  14273  gsum2dfi  14274  srglmhm  14405  srgrmhm  14406  ringlghm  14474  ringrghm  14475  gsumfsum  15033  expghmap  15052  snifpsrbagfi  15170  fczpsrbag  15171  psrass1filem  15182  rhmpsrfilem2  15190  psrmulvalfi  15193  psrmulclfilem  15194  psrlidmfi  15204  psrridmfi  15205  mvrffi  15214  mplsubgfilemm  15226  tgrest  15407  resttopon  15409  rest0  15417  cnpfval  15433  txcnp  15509  uptx  15512  cnmpt11  15521  bdxmet  15739  cncfmptc  15834  cncfmptid  15835  cdivcncfap  15842  mulcncf  15846  maxcncf  15853  mincncf  15854  ivthreinc  15883  hovercncf  15884  limcmpted  15901  dvfgg  15926  dvcnp2cntop  15937  dvmulxxbr  15940  dvcjbr  15946  dvexp  15949  dvrecap  15951  dvmptclx  15956  dvmptaddx  15957  dvmptmulx  15958  dvmptcjx  15962  dvef  15965  elply2  15973  plyf  15975  elplyd  15979  dvply2g  16004  lgseisenlem3  16408  lgseisenlem4  16409  incistruhgr  16548  pw1map  17242  subctctexmid  17247  nninffeq  17281  iswomni0  17320  dceqnconst  17329  dcapnconst  17330