Theorem fnconstg 6770

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 6769	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2	1	ffnd 6710	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  {csn 4584   × cxp 5648   Fn wfn 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  fconst2g  7209  ofc1  7721  ofc2  7722  caofid0l  7726  caofid0r  7727  caofid1  7728  caofid2  7729  fnsuppres  8211  fczsupp0  8213  fczfsuppd  9381  brwdom2  9570  cantnf0  9679  ofnegsub  12321  ofsubge0  12322  pwsplusgval  17667  pwsmulrval  17668  pwsvscafval  17671  pwsco1mhm  19033  dprdsubg  20245  pwsmgp  20561  pwssplit1  21339  frlmpwsfi  22063  frlmbas  22066  frlmvscaval  22079  islindf4  22149  psrascl  22291  matunitlindflem1  22999  matunitlindflem2  23000  tmdgsum2  24420  0plef  25998  0pledm  25999  itg1ge0  26012  mbfi1fseqlem5  26045  xrge0f  26057  itg2ge0  26061  itg2addlem  26084  bddibl  26165  dvidlem  26240  rolle  26315  dveq0  26325  dv11cn  26326  tdeglem4  26383  mdeg0  26393  fta1blem  26494  rnplynfin  26635  qaa  26652  basellem9  27421  noextendseq  28029  noetainflem4  28102  constcof  33262  fdifsuppconst  33329  elrspunidl  34024  ofcc  34784  ofcof  34785  eulerpartlemt  35049  ptrecube  38631  poimirlem1  38632  poimirlem2  38633  poimirlem3  38634  poimirlem4  38635  poimirlem5  38636  poimirlem6  38637  poimirlem7  38638  poimirlem10  38641  poimirlem11  38642  poimirlem12  38643  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  poimirlem22  38653  poimirlem23  38654  poimirlem28  38659  poimirlem29  38660  poimirlem31  38662  poimirlem32  38663  broucube  38665  cnpwstotbnd  38824  eqlkr2  40250  fsuppssind  43714  pwssplit4  44184  mpaaeu  44245  rngunsnply  44264  ofoaid1  44453  ofoaid2  44454  naddcnffo  44459  ofdivrec  45403  dvconstbi  45411  sqrtnnaa  48006  sqrtnzqaa  48007  zlmodzxzscm  49562  nelsubclem  50274  aacllem  51107  veroquadmodzerod  51152