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 689	1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  Vcvv 3470  {csn 4624   × cxp 5670  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550

This theorem is referenced by:  ovconst2  7595  mapsncnv  8905  ofsubeq0  12233  ofsubge0  12235  ser0f  14046  hashinf  14320  iserge0  15633  iseraltlem1  15654  sum0  15693  sumz  15694  harmonic  15831  prodf1f  15864  fprodntriv  15912  prod1  15914  setcmon  18069  0mhm  18764  mulgfval  19018  mulgpropd  19064  dprdsubg  19974  pwspjmhmmgpd  20257  0lmhm  20918  frlmlmod  21676  frlmlss  21678  frlmbas  21682  frlmip  21705  islindf4  21765  mplsubglem  21934  coe1tm  22185  mdetuni0  22516  txkgen  23549  xkofvcn  23581  nmo0  24645  pcorevlem  24946  rrxip  25311  mbfpos  25573  0pval  25593  0pledm  25595  xrge0f  25654  itg2ge0  25658  ibl0  25709  bddibl  25762  dvcmul  25868  dvef  25905  rolle  25915  dveq0  25926  dv11cn  25927  ftc2  25972  tdeglem4  25988  tdeglem4OLD  25989  ply1rem  26093  fta1g  26097  fta1blem  26098  0dgrb  26173  dgrnznn  26174  dgrlt  26194  plymul0or  26208  plydivlem4  26224  plyrem  26233  fta1  26236  vieta1lem2  26239  elqaalem3  26249  aaliou2  26268  ulmdvlem1  26329  dchrelbas2  27163  dchrisumlem3  27417  noetasuplem4  27662  noetainflem4  27666  axlowdimlem9  28754  axlowdimlem12  28757  axlowdimlem17  28762  0oval  30591  occllem  31106  ho01i  31631  0cnfn  31783  0lnfn  31788  nmfn0  31790  nlelchi  31864  opsqrlem2  31944  opsqrlem4  31946  opsqrlem5  31947  hmopidmchi  31954  elrspunidl  33138  lbsdiflsp0  33314  evls1maprnss  33365  breprexpnat  34260  circlemethnat  34267  circlevma  34268  connpconn  34839  txsconnlem  34844  cvxsconn  34847  cvmliftphtlem  34921  fullfunfv  35537  matunitlindflem1  37083  matunitlindflem2  37084  ptrecube  37087  poimirlem1  37088  poimirlem2  37089  poimirlem3  37090  poimirlem4  37091  poimirlem5  37092  poimirlem6  37093  poimirlem7  37094  poimirlem10  37097  poimirlem11  37098  poimirlem12  37099  poimirlem16  37103  poimirlem17  37104  poimirlem19  37106  poimirlem20  37107  poimirlem22  37109  poimirlem23  37110  poimirlem28  37115  poimirlem29  37116  poimirlem30  37117  poimirlem31  37118  poimirlem32  37119  poimir  37120  broucube  37121  mblfinlem2  37125  itg2addnclem  37138  itg2addnc  37141  ftc1anclem5  37164  ftc2nc  37169  cnpwstotbnd  37264  lfl0f  38535  eqlkr2  38566  lcd0vvalN  41080  frlm0vald  41763  evlsvvval  41790  selvvvval  41812  evlselv  41814  mzpsubst  42162  mzpcompact2lem  42165  mzpcong  42387  hbtlem2  42542  mncn0  42557  mpaaeu  42568  aaitgo  42580  rngunsnply  42591  cantnfresb  42747  hashnzfzclim  43753  ofsubid  43755  dvconstbi  43765  binomcxplemnotnn0  43787  n0p  44401  snelmap  44442  fvconst0ci  47905  fvconstdomi  47906  aacllem  48228

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »