Theorem fnconstg 6552

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

Step	Hyp	Ref	Expression
1		fconstg 6551	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2	1	ffnd 6499	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111  {csn 4522   × cxp 5522   Fn wfn 6330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-fun 6337  df-fn 6338  df-f 6339

This theorem is referenced by:  fconst2g  6956  ofc1  7430  ofc2  7431  caofid0l  7435  caofid0r  7436  caofid1  7437  caofid2  7438  fnsuppres  7865  fczsupp0  7867  fczfsuppd  8884  brwdom2  9070  cantnf0  9171  ofnegsub  11672  ofsubge0  11673  pwsplusgval  16821  pwsmulrval  16822  pwsvscafval  16825  pwsco1mhm  18062  dprdsubg  19214  pwsmgp  19439  pwssplit1  19899  frlmpwsfi  20517  frlmbas  20520  frlmvscaval  20533  islindf4  20603  tmdgsum2  22796  0plef  24372  0pledm  24373  itg1ge0  24386  mbfi1fseqlem5  24419  xrge0f  24431  itg2ge0  24435  itg2addlem  24458  bddibl  24539  dvidlem  24614  rolle  24689  dveq0  24699  dv11cn  24700  tdeglem4  24759  tdeglem4OLD  24760  mdeg0  24770  fta1blem  24868  qaa  25018  basellem9  25773  fdifsuppconst  30547  elrspunidl  31127  ofcc  31593  ofcof  31594  eulerpartlemt  31857  noextendseq  33435  noetainflem4  33508  matunitlindflem1  35333  matunitlindflem2  35334  ptrecube  35337  poimirlem1  35338  poimirlem2  35339  poimirlem3  35340  poimirlem4  35341  poimirlem5  35342  poimirlem6  35343  poimirlem7  35344  poimirlem10  35347  poimirlem11  35348  poimirlem12  35349  poimirlem16  35353  poimirlem17  35354  poimirlem19  35356  poimirlem20  35357  poimirlem22  35359  poimirlem23  35360  poimirlem28  35365  poimirlem29  35366  poimirlem31  35368  poimirlem32  35369  broucube  35371  cnpwstotbnd  35515  eqlkr2  36676  fsuppssind  39787  mhphf  39790  pwssplit4  40406  mpaaeu  40467  rngunsnply  40490  ofdivrec  41403  dvconstbi  41411  zlmodzxzscm  45126  aacllem  45720