MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnconstg Unicode version

Theorem fnconstg 5467
Description: A cross product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.)
Assertion
Ref Expression
fnconstg  |-  ( B  e.  V  ->  ( A  X.  { B }
)  Fn  A )

Proof of Theorem fnconstg
StepHypRef Expression
1 fconstg 5466 . 2  |-  ( B  e.  V  ->  ( A  X.  { B }
) : A --> { B } )
2 ffn 5427 . 2  |-  ( ( A  X.  { B } ) : A --> { B }  ->  ( A  X.  { B }
)  Fn  A )
31, 2syl 15 1  |-  ( B  e.  V  ->  ( A  X.  { B }
)  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1701   {csn 3674    X. cxp 4724    Fn wfn 5287   -->wf 5288
This theorem is referenced by:  fconst2g  5767  fnsuppres  5773  ofc1  6142  ofc2  6143  caofid0l  6147  caofid0r  6148  caofid1  6149  caofid2  6150  brwdom2  7332  ofnegsub  9789  ofsubge0  9790  pwsplusgval  13438  pwsmulrval  13439  pwsvscafval  13442  xpsc0  13511  xpsc1  13512  pwsco1mhm  14495  dprdsubg  15308  pwsmgp  15450  tmdgsum2  17831  0plef  19080  0pledm  19081  itg1ge0  19094  mbfi1fseqlem5  19127  xrge0f  19139  itg2ge0  19143  itg2addlem  19166  bddibl  19247  dvidlem  19318  rolle  19390  dveq0  19400  dv11cn  19401  tdeglem4  19499  fta1blem  19607  qaa  19756  basellem9  20379  ofcc  23665  cnpwstotbnd  25669  pwssplit1  26336  pwssplit4  26339  frlmpwsfi  26368  frlmbas  26371  frlmvscaval  26379  islindf4  26456  mpaaeu  26503  rngunsnply  26526  ofdivrec  26691  dvconstbi  26699  eqlkr2  29108
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-fun 5294  df-fn 5295  df-f 5296
  Copyright terms: Public domain W3C validator