Theorem fvconst2 7088

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 7086	. 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
3	1, 2	mpan 687	1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  Vcvv 3433  {csn 4562   × cxp 5588  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445

This theorem is referenced by:  ovconst2  7461  mapsncnv  8690  ofsubeq0  11979  ofsubge0  11981  ser0f  13785  hashinf  14058  iserge0  15381  iseraltlem1  15402  sum0  15442  sumz  15443  harmonic  15580  prodf1f  15613  fprodntriv  15661  prod1  15663  setcmon  17811  0mhm  18467  mulgfval  18711  mulgpropd  18754  dprdsubg  19636  0lmhm  20311  frlmlmod  20965  frlmlss  20967  frlmbas  20971  frlmip  20994  islindf4  21054  mplsubglem  21214  coe1tm  21453  mdetuni0  21779  txkgen  22812  xkofvcn  22844  nmo0  23908  pcorevlem  24198  rrxip  24563  mbfpos  24824  0pval  24844  0pledm  24846  xrge0f  24905  itg2ge0  24909  ibl0  24960  bddibl  25013  dvcmul  25117  dvef  25153  rolle  25163  dveq0  25173  dv11cn  25174  ftc2  25217  tdeglem4  25233  tdeglem4OLD  25234  ply1rem  25337  fta1g  25341  fta1blem  25342  0dgrb  25416  dgrnznn  25417  dgrlt  25436  plymul0or  25450  plydivlem4  25465  plyrem  25474  fta1  25477  vieta1lem2  25480  elqaalem3  25490  aaliou2  25509  ulmdvlem1  25568  dchrelbas2  26394  dchrisumlem3  26648  axlowdimlem9  27327  axlowdimlem12  27330  axlowdimlem17  27335  0oval  29159  occllem  29674  ho01i  30199  0cnfn  30351  0lnfn  30356  nmfn0  30358  nlelchi  30432  opsqrlem2  30512  opsqrlem4  30514  opsqrlem5  30515  hmopidmchi  30522  elrspunidl  31615  lbsdiflsp0  31716  breprexpnat  32623  circlemethnat  32630  circlevma  32631  connpconn  33206  txsconnlem  33211  cvxsconn  33214  cvmliftphtlem  33288  noetasuplem4  33948  noetainflem4  33952  fullfunfv  34258  matunitlindflem1  35782  matunitlindflem2  35783  ptrecube  35786  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem28  35814  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  poimir  35819  broucube  35820  mblfinlem2  35824  itg2addnclem  35837  itg2addnc  35840  ftc1anclem5  35863  ftc2nc  35868  cnpwstotbnd  35964  lfl0f  37090  eqlkr2  37121  lcd0vvalN  39634  frlm0vald  40269  pwspjmhmmgpd  40274  mhphf  40292  mzpsubst  40577  mzpcompact2lem  40580  mzpcong  40801  hbtlem2  40956  mncn0  40971  mpaaeu  40982  aaitgo  40994  rngunsnply  41005  hashnzfzclim  41947  ofsubid  41949  dvconstbi  41959  binomcxplemnotnn0  41981  n0p  42598  snelmap  42639  fvconst0ci  46197  fvconstdomi  46198  aacllem  46516