Theorem fnconstg 6792

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  {csn 4588   × cxp 5653   Fn wfn 6553

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6560  df-fn 6561  df-f 6562

This theorem is used by:  fconst2g  7232  ofc1  7745  ofc2  7746  caofid0l  7750  caofid0r  7751  caofid1  7752  caofid2  7753  fnsuppres  8236  fczsupp0  8238  fczfsuppd  9405  brwdom2  9594  cantnf0  9703  ofnegsub  12345  ofsubge0  12346  pwsplusgval  17691  pwsmulrval  17692  pwsvscafval  17695  pwsco1mhm  19057  dprdsubg  20270  pwsmgp  20586  pwssplit1  21364  frlmpwsfi  22088  frlmbas  22091  frlmvscaval  22104  islindf4  22174  psrascl  22316  matunitlindflem1  23024  matunitlindflem2  23025  tmdgsum2  24445  0plef  26023  0pledm  26024  itg1ge0  26037  mbfi1fseqlem5  26070  xrge0f  26082  itg2ge0  26086  itg2addlem  26109  bddibl  26190  dvidlem  26265  rolle  26340  dveq0  26350  dv11cn  26351  tdeglem4  26408  mdeg0  26418  fta1blem  26519  rnplynfin  26660  qaa  26677  basellem9  27446  noextendseq  28054  noetainflem4  28127  constcof  33287  fdifsuppconst  33353  elrspunidl  34048  ofcc  34808  ofcof  34809  eulerpartlemt  35073  ptrecube  38730  poimirlem1  38731  poimirlem2  38732  poimirlem3  38733  poimirlem4  38734  poimirlem5  38735  poimirlem6  38736  poimirlem7  38737  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem22  38752  poimirlem23  38753  poimirlem28  38758  poimirlem29  38759  poimirlem31  38761  poimirlem32  38762  broucube  38764  cnpwstotbnd  38923  eqlkr2  40349  fsuppssind  43814  pwssplit4  44284  mpaaeu  44344  rngunsnply  44363  ofoaid1  44552  ofoaid2  44553  naddcnffo  44558  ofdivrec  45502  dvconstbi  45510  sqrtnnaa  48118  sqrtnzqaa  48119  zlmodzxzscm  49674  nelsubclem  50386  aacllem  51219  veroquadmodzerod  51264