Theorem fvconst2 6966

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

Hypothesis

Ref	Expression
fvconst2.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
fvconst2	⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Proof of Theorem fvconst2

Step	Hyp	Ref	Expression
1		fvconst2.1	. 2 ⊢ 𝐵 ∈ V
2		fvconst2g 6964	. 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
3	1, 2	mpan 688	1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3494  {csn 4567   × cxp 5553  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363

This theorem is referenced by:  ovconst2  7328  mapsncnv  8457  ofsubeq0  11635  ofsubge0  11637  ser0f  13424  hashinf  13696  iserge0  15017  iseraltlem1  15038  sum0  15078  sumz  15079  harmonic  15214  prodf1f  15248  fprodntriv  15296  prod1  15298  setcmon  17347  0mhm  17984  mulgfval  18226  mulgpropd  18269  dprdsubg  19146  0lmhm  19812  mplsubglem  20214  coe1tm  20441  frlmlmod  20893  frlmlss  20895  frlmbas  20899  frlmip  20922  islindf4  20982  mdetuni0  21230  txkgen  22260  xkofvcn  22292  nmo0  23344  pcorevlem  23630  rrxip  23993  mbfpos  24252  0pval  24272  0pledm  24274  xrge0f  24332  itg2ge0  24336  ibl0  24387  bddibl  24440  dvcmul  24541  dvef  24577  rolle  24587  dveq0  24597  dv11cn  24598  ftc2  24641  tdeglem4  24654  ply1rem  24757  fta1g  24761  fta1blem  24762  0dgrb  24836  dgrnznn  24837  dgrlt  24856  plymul0or  24870  plydivlem4  24885  plyrem  24894  fta1  24897  vieta1lem2  24900  elqaalem3  24910  aaliou2  24929  ulmdvlem1  24988  dchrelbas2  25813  dchrisumlem3  26067  axlowdimlem9  26736  axlowdimlem12  26739  axlowdimlem17  26744  0oval  28565  occllem  29080  ho01i  29605  0cnfn  29757  0lnfn  29762  nmfn0  29764  nlelchi  29838  opsqrlem2  29918  opsqrlem4  29920  opsqrlem5  29921  hmopidmchi  29928  lbsdiflsp0  31022  breprexpnat  31905  circlemethnat  31912  circlevma  31913  connpconn  32482  txsconnlem  32487  cvxsconn  32490  cvmliftphtlem  32564  noetalem3  33219  fullfunfv  33408  matunitlindflem1  34903  matunitlindflem2  34904  ptrecube  34907  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem28  34935  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  poimir  34940  broucube  34941  mblfinlem2  34945  itg2addnclem  34958  itg2addnc  34961  ftc1anclem5  34986  ftc2nc  34991  cnpwstotbnd  35090  lfl0f  36220  eqlkr2  36251  lcd0vvalN  38764  uvcn0  39171  mzpsubst  39365  mzpcompact2lem  39368  mzpcong  39589  hbtlem2  39744  mncn0  39759  mpaaeu  39770  aaitgo  39782  rngunsnply  39793  hashnzfzclim  40674  ofsubid  40676  dvconstbi  40686  binomcxplemnotnn0  40708  n0p  41325  snelmap  41366  aacllem  44922