Theorem fvconst2 7178

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {csn 4589   × cxp 5636  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  ovconst2  7569  mapsncnv  8866  ofsubeq0  12183  ofsubge0  12185  ser0f  14020  hashinf  14300  iserge0  15627  iseraltlem1  15648  sum0  15687  sumz  15688  harmonic  15825  prodf1f  15858  fprodntriv  15908  prod1  15910  setcmon  18049  0mhm  18746  mulgfval  19001  mulgpropd  19048  dprdsubg  19956  pwspjmhmmgpd  20237  0lmhm  20947  frlmlmod  21658  frlmlss  21660  frlmbas  21664  frlmip  21687  islindf4  21747  mplsubglem  21908  psdmvr  22056  coe1tm  22159  evls1maprnss  22265  mdetuni0  22508  txkgen  23539  xkofvcn  23571  nmo0  24623  pcorevlem  24926  rrxip  25290  mbfpos  25552  0pval  25572  0pledm  25574  xrge0f  25632  itg2ge0  25636  ibl0  25688  bddibl  25741  dvcmul  25847  dvef  25884  rolle  25894  dveq0  25905  dv11cn  25906  ftc2  25951  tdeglem4  25965  ply1rem  26071  fta1g  26075  fta1blem  26076  0dgrb  26151  dgrnznn  26152  dgrlt  26172  plymul0or  26188  plydivlem4  26204  plyrem  26213  fta1  26216  vieta1lem2  26219  elqaalem3  26229  aaliou2  26248  ulmdvlem1  26309  dchrelbas2  27148  dchrisumlem3  27402  noetasuplem4  27648  noetainflem4  27652  axlowdimlem9  28877  axlowdimlem12  28880  axlowdimlem17  28885  0oval  30717  occllem  31232  ho01i  31757  0cnfn  31909  0lnfn  31914  nmfn0  31916  nlelchi  31990  opsqrlem2  32070  opsqrlem4  32072  opsqrlem5  32073  hmopidmchi  32080  elrspunidl  33399  coe1zfv  33556  lbsdiflsp0  33622  breprexpnat  34625  circlemethnat  34632  circlevma  34633  connpconn  35222  txsconnlem  35227  cvxsconn  35230  cvmliftphtlem  35304  fullfunfv  35935  matunitlindflem1  37610  matunitlindflem2  37611  ptrecube  37614  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem28  37642  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  poimir  37647  broucube  37648  mblfinlem2  37652  itg2addnclem  37665  itg2addnc  37668  ftc1anclem5  37691  ftc2nc  37696  cnpwstotbnd  37791  lfl0f  39062  eqlkr2  39093  lcd0vvalN  41607  frlm0vald  42527  evlsvvval  42551  selvvvval  42573  evlselv  42575  mzpsubst  42736  mzpcompact2lem  42739  mzpcong  42961  hbtlem2  43113  mncn0  43128  mpaaeu  43139  aaitgo  43151  rngunsnply  43158  cantnfresb  43313  hashnzfzclim  44311  ofsubid  44313  dvconstbi  44323  binomcxplemnotnn0  44345  n0p  45039  snelmap  45076  cjnpoly  46890  sinnpoly  46892  fvconst0ci  48879  fvconstdomi  48880  islmd  49654  iscmd  49655  aacllem  49790