Theorem fvconst2g 5923

Description: The value of a constant function. (Contributed by NM, 20-Aug-2005.)

Assertion

Ref	Expression
fvconst2g	⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Proof of Theorem fvconst2g

Step	Hyp	Ref	Expression
1		fconstg 5587	. 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		fvconst 5897	. 2 ⊢ (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
3	1, 2	sylan 283	1 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  {csn 3708   × cxp 4770  ⟶wf 5371  ‘cfv 5375

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 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 4247  ax-pow 4309  ax-pr 4344

This theorem 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-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-mpt 4192  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-fv 5383

This theorem is referenced by:  fconst2g  5924  fvconst2  5925  ofc1g  6318  ofc2g  6319  caofid0l  6323  caofid0r  6324  caofid1  6325  caofid2  6326  fczsupp0  6493  ser0  10953  exp3vallem  10960  exp3val  10961  exp1  10965  expp1  10966  resqrexlem1arp  11754  resqrexlemf1  11757  climconst2  12040  climaddc1  12078  climmulc2  12080  climsubc1  12081  climsubc2  12082  climlec2  12090  prodf1  12292  prod0  12335  ialgrlemconst  12804  ialgr0  12805  algrf  12806  algrp1  12807  0mhm  13776  mulgval  13908  mulgfng  13910  mulgnngzsum  13913  mulg1  13915  mulgnnp1  13916  mulgnnsubcl  13920  mulgnn0z  13935  mulgnndir  13937  gsumconstcmn  14149  pwsbas  14188  pwsplusgval  14191  pwsmulrval  14192  pwsinvg  14198  mplsubgfilemm  15072  lmconst  15300  cnconst2  15317  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvconst  15778  dvconstre  15780  dvconstss  15782  dvef  15811