Theorem fvconst2 7210

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450  {csn 4584   × cxp 5648  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is used by:  ovconst2  7601  mapsncnv  8924  ofsubeq0  12320  ofsubge0  12322  ser0f  14201  hashinf  14482  iserge0  15833  iseraltlem1  15854  sum0  15892  sumz  15893  harmonic  16033  prodf1f  16066  fprodntriv  16114  prod1  16116  setcmon  18267  0mhm  19020  mulgfval  19284  mulgpropd  19331  dprdsubg  20245  pwspjmhmmgpd  20562  0lmhm  21320  frlmlmod  22060  frlmlss  22062  frlmbas  22066  frlmip  22089  islindf4  22149  mplsubglem  22311  evlsvvval  22407  selvvvval  22456  psdmvr  22495  coe1tm  22597  evls1maprnss  22701  mdetuni0  22941  matunitlindflem1  22999  matunitlindflem2  23000  txkgen  23976  xkofvcn  24008  nmo0  25059  pcorevlem  25352  rrxip  25716  mbfpos  25977  0pval  25997  0pledm  25999  xrge0f  26057  itg2ge0  26061  ibl0  26112  bddibl  26165  dvcmul  26269  dvef  26305  rolle  26315  dveq0  26325  dv11cn  26326  ftc2  26369  tdeglem4  26383  ply1rem  26489  fta1g  26493  fta1blem  26494  0dgrb  26570  dgrnznn  26571  dgrlt  26590  plymul0or  26604  plydivlem4  26622  plyrem  26631  fta1  26634  rnplynfin  26635  vieta1lem2  26639  elqaalem3  26649  aaliou2  26672  ulmdvlem1  26732  dchrelbas2  27569  dchrisumlem3  27823  noetasuplem4  28098  noetainflem4  28102  axlowdimlem9  29533  axlowdimlem12  29536  axlowdimlem17  29541  0oval  31395  occllem  31910  ho01i  32435  0cnfn  32587  0lnfn  32592  nmfn0  32594  nlelchi  32668  opsqrlem2  32748  opsqrlem4  32750  opsqrlem5  32751  hmopidmchi  32758  elrspunidl  34024  coe1zfv  34168  psrnzr  34190  selvascl  34195  selvply1rhm0  34204  mplvrpmmhm  34224  vieta  34258  lbsdiflsp0  34304  breprexpnat  35309  circlemethnat  35316  circlevma  35317  connpconn  36086  txsconnlem  36091  cvxsconn  36094  cvmliftphtlem  36168  fullfunfv  36803  ptrecube  38631  poimirlem1  38632  poimirlem2  38633  poimirlem3  38634  poimirlem4  38635  poimirlem5  38636  poimirlem6  38637  poimirlem7  38638  poimirlem10  38641  poimirlem11  38642  poimirlem12  38643  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  poimirlem22  38653  poimirlem23  38654  poimirlem28  38659  poimirlem29  38660  poimirlem30  38661  poimirlem31  38662  poimirlem32  38663  poimir  38664  broucube  38665  mblfinlem2  38669  itg2addnclem  38682  itg2addnc  38685  ftc1anclem5  38708  ftc2nc  38713  cnpwstotbnd  38824  lfl0f  40219  eqlkr2  40250  lcd0vvalN  42763  frlm0vald  43696  evlselv  43710  mzpsubst  43852  mzpcompact2lem  43855  mzpcong  44072  hbtlem2  44219  mncn0  44234  mpaaeu  44245  aaitgo  44257  rngunsnply  44264  cantnfresb  44419  hashnzfzclim  45399  ofsubid  45401  dvconstbi  45411  binomcxplemnotnn0  45433  n0p  46155  snelmap  46192  cjnpoly  48032  sinnpoly  48034  fvconst0ci  50098  fvconstdomi  50099  par2diag  50873  islmd  50941  iscmd  50942  aacllem  51107  veroquadmodzerod  51152