MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvconst2 Structured version   Visualization version   GIF version

Theorem fvconst2 6958
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
StepHypRef Expression
1 fvconst2.1 . 2 𝐵 ∈ V
2 fvconst2g 6956 . 2 ((𝐵 ∈ V ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2mpan 686 1 (𝐶𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  Vcvv 3492  {csn 4557   × cxp 5546  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356
This theorem is referenced by:  ovconst2  7317  mapsncnv  8445  ofsubeq0  11623  ofsubge0  11625  ser0f  13411  hashinf  13683  iserge0  15005  iseraltlem1  15026  sum0  15066  sumz  15067  harmonic  15202  prodf1f  15236  fprodntriv  15284  prod1  15286  setcmon  17335  0mhm  17972  mulgfval  18164  mulgpropd  18207  dprdsubg  19075  0lmhm  19741  mplsubglem  20142  coe1tm  20369  frlmlmod  20821  frlmlss  20823  frlmbas  20827  frlmip  20850  islindf4  20910  mdetuni0  21158  txkgen  22188  xkofvcn  22220  nmo0  23271  pcorevlem  23557  rrxip  23920  mbfpos  24179  0pval  24199  0pledm  24201  xrge0f  24259  itg2ge0  24263  ibl0  24314  bddibl  24367  dvcmul  24468  dvef  24504  rolle  24514  dveq0  24524  dv11cn  24525  ftc2  24568  tdeglem4  24581  ply1rem  24684  fta1g  24688  fta1blem  24689  0dgrb  24763  dgrnznn  24764  dgrlt  24783  plymul0or  24797  plydivlem4  24812  plyrem  24821  fta1  24824  vieta1lem2  24827  elqaalem3  24837  aaliou2  24856  ulmdvlem1  24915  dchrelbas2  25740  dchrisumlem3  25994  axlowdimlem9  26663  axlowdimlem12  26666  axlowdimlem17  26671  0oval  28492  occllem  29007  ho01i  29532  0cnfn  29684  0lnfn  29689  nmfn0  29691  nlelchi  29765  opsqrlem2  29845  opsqrlem4  29847  opsqrlem5  29848  hmopidmchi  29855  lbsdiflsp0  30921  breprexpnat  31804  circlemethnat  31811  circlevma  31812  connpconn  32379  txsconnlem  32384  cvxsconn  32387  cvmliftphtlem  32461  noetalem3  33116  fullfunfv  33305  matunitlindflem1  34769  matunitlindflem2  34770  ptrecube  34773  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem4  34777  poimirlem5  34778  poimirlem6  34779  poimirlem7  34780  poimirlem10  34783  poimirlem11  34784  poimirlem12  34785  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem22  34795  poimirlem23  34796  poimirlem28  34801  poimirlem29  34802  poimirlem30  34803  poimirlem31  34804  poimirlem32  34805  poimir  34806  broucube  34807  mblfinlem2  34811  itg2addnclem  34824  itg2addnc  34827  ftc1anclem5  34852  ftc2nc  34857  cnpwstotbnd  34956  lfl0f  36085  eqlkr2  36116  lcd0vvalN  38629  uvcn0  39029  mzpsubst  39223  mzpcompact2lem  39226  mzpcong  39447  hbtlem2  39602  mncn0  39617  mpaaeu  39628  aaitgo  39640  rngunsnply  39651  hashnzfzclim  40531  ofsubid  40533  dvconstbi  40543  binomcxplemnotnn0  40565  n0p  41182  snelmap  41223  aacllem  44830
  Copyright terms: Public domain W3C validator