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

Theorem fconst6 6309
Description: A constant function as a mapping. (Contributed by Jeff Madsen, 30-Nov-2009.) (Revised by Mario Carneiro, 22-Apr-2015.)
Hypothesis
Ref Expression
fconst6.1 𝐵𝐶
Assertion
Ref Expression
fconst6 (𝐴 × {𝐵}):𝐴𝐶

Proof of Theorem fconst6
StepHypRef Expression
1 fconst6.1 . 2 𝐵𝐶
2 fconst6g 6308 . 2 (𝐵𝐶 → (𝐴 × {𝐵}):𝐴𝐶)
31, 2ax-mp 5 1 (𝐴 × {𝐵}):𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  {csn 4367   × cxp 5309  wf 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pr 5096
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-ral 3093  df-rab 3097  df-v 3386  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4843  df-opab 4905  df-mpt 4922  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-fun 6102  df-fn 6103  df-f 6104
This theorem is referenced by:  ramz  16059  psrlidm  19723  psrbag0  19813  00ply1bas  19929  ply1plusgfvi  19931  mbfpos  23756  i1f0  23792  axlowdimlem1  26172  axlowdimlem7  26178  axlowdim1  26189  hlim0  28610  0cnfn  29357  0lnfn  29362  circlemethnat  31232  circlevma  31233  noxp1o  32322  poimirlem29  33920  poimirlem30  33921  poimirlem31  33922  poimir  33924  broucube  33925  expgrowth  39305
  Copyright terms: Public domain W3C validator