Theorem fnconstg 6767

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {csn 4587   × cxp 5657   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  fconst2g  7206  ofc1  7710  ofc2  7711  caofid0l  7715  caofid0r  7716  caofid1  7717  caofid2  7718  fnsuppres  8193  fczsupp0  8195  fczfsuppd  9360  brwdom2  9549  cantnf0  9658  ofnegsub  12244  ofsubge0  12245  pwsplusgval  17582  pwsmulrval  17583  pwsvscafval  17586  pwsco1mhm  18947  dprdsubg  20159  pwsmgp  20473  pwssplit1  21249  frlmpwsfi  21971  frlmbas  21974  frlmvscaval  21987  islindf4  22057  psrascl  22199  matunitlindflem1  22907  matunitlindflem2  22908  tmdgsum2  24328  0plef  25906  0pledm  25907  itg1ge0  25920  mbfi1fseqlem5  25953  xrge0f  25965  itg2ge0  25969  itg2addlem  25992  bddibl  26074  dvidlem  26149  rolle  26224  dveq0  26234  dv11cn  26235  tdeglem4  26292  mdeg0  26302  fta1blem  26403  rnplynfin  26546  qaa  26563  basellem9  27333  noextendseq  27911  noetainflem4  27984  constcof  33102  fdifsuppconst  33169  elrspunidl  33864  ofcc  34624  ofcof  34625  eulerpartlemt  34890  ptrecube  38377  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem5  38382  poimirlem6  38383  poimirlem7  38384  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem23  38400  poimirlem28  38405  poimirlem29  38406  poimirlem31  38408  poimirlem32  38409  broucube  38411  cnpwstotbnd  38555  eqlkr2  39981  fsuppssind  43447  pwssplit4  43938  mpaaeu  43999  rngunsnply  44018  ofoaid1  44207  ofoaid2  44208  naddcnffo  44213  ofdivrec  45158  dvconstbi  45166  sqrtnnaa  47739  sqrtnzqaa  47740  zlmodzxzscm  49295  nelsubclem  50001  aacllem  50780  veroquadmodzerod  50825