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

Theorem fnconstg 6731
Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.)
Assertion
Ref Expression
fnconstg (𝐵𝑉 → (𝐴 × {𝐵}) Fn 𝐴)

Proof of Theorem fnconstg
StepHypRef Expression
1 fconstg 6730 . 2 (𝐵𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
21ffnd 6670 1 (𝐵𝑉 → (𝐴 × {𝐵}) Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  {csn 4587   × cxp 5632   Fn wfn 6492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  fconst2g  7153  ofc1  7644  ofc2  7645  caofid0l  7649  caofid0r  7650  caofid1  7651  caofid2  7652  fnsuppres  8123  fczsupp0  8125  fczfsuppd  9324  brwdom2  9510  cantnf0  9612  ofnegsub  12152  ofsubge0  12153  pwsplusgval  17373  pwsmulrval  17374  pwsvscafval  17377  pwsco1mhm  18643  dprdsubg  19804  pwsmgp  20043  pwssplit1  20523  frlmpwsfi  21161  frlmbas  21164  frlmvscaval  21177  islindf4  21247  tmdgsum2  23450  0plef  25039  0pledm  25040  itg1ge0  25053  mbfi1fseqlem5  25087  xrge0f  25099  itg2ge0  25103  itg2addlem  25126  bddibl  25207  dvidlem  25282  rolle  25357  dveq0  25367  dv11cn  25368  tdeglem4  25427  tdeglem4OLD  25428  mdeg0  25438  fta1blem  25536  qaa  25686  basellem9  26441  noextendseq  27018  noetainflem4  27091  fdifsuppconst  31607  elrspunidl  32206  ofcc  32708  ofcof  32709  eulerpartlemt  32974  matunitlindflem1  36077  matunitlindflem2  36078  ptrecube  36081  poimirlem1  36082  poimirlem2  36083  poimirlem3  36084  poimirlem4  36085  poimirlem5  36086  poimirlem6  36087  poimirlem7  36088  poimirlem10  36091  poimirlem11  36092  poimirlem12  36093  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem22  36103  poimirlem23  36104  poimirlem28  36109  poimirlem29  36110  poimirlem31  36112  poimirlem32  36113  broucube  36115  cnpwstotbnd  36259  eqlkr2  37565  fsuppssind  40771  mhphf  40774  pwssplit4  41419  mpaaeu  41480  rngunsnply  41503  ofoaid1  41675  ofoaid2  41676  naddcnffo  41681  ofdivrec  42613  dvconstbi  42621  zlmodzxzscm  46440  aacllem  47255
  Copyright terms: Public domain W3C validator