Theorem fnconstg 6762

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {csn 4584   × cxp 5649   Fn wfn 6526

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 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  fconst2g  7201  ofc1  7710  ofc2  7711  caofid0l  7715  caofid0r  7716  caofid1  7717  caofid2  7718  fnsuppres  8192  fczsupp0  8194  fczfsuppd  9362  brwdom2  9551  cantnf0  9660  ofnegsub  12299  ofsubge0  12300  pwsplusgval  17642  pwsmulrval  17643  pwsvscafval  17646  pwsco1mhm  19008  dprdsubg  20220  pwsmgp  20536  pwssplit1  21314  frlmpwsfi  22038  frlmbas  22041  frlmvscaval  22054  islindf4  22124  psrascl  22266  matunitlindflem1  22974  matunitlindflem2  22975  tmdgsum2  24395  0plef  25973  0pledm  25974  itg1ge0  25987  mbfi1fseqlem5  26020  xrge0f  26032  itg2ge0  26036  itg2addlem  26059  bddibl  26140  dvidlem  26215  rolle  26290  dveq0  26300  dv11cn  26301  tdeglem4  26358  mdeg0  26368  fta1blem  26469  rnplynfin  26612  qaa  26629  basellem9  27398  noextendseq  28006  noetainflem4  28079  constcof  33197  fdifsuppconst  33264  elrspunidl  33960  ofcc  34720  ofcof  34721  eulerpartlemt  34986  ptrecube  38506  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem22  38528  poimirlem23  38529  poimirlem28  38534  poimirlem29  38535  poimirlem31  38537  poimirlem32  38538  broucube  38540  cnpwstotbnd  38699  eqlkr2  40125  fsuppssind  43583  pwssplit4  44049  mpaaeu  44110  rngunsnply  44129  ofoaid1  44318  ofoaid2  44319  naddcnffo  44324  ofdivrec  45269  dvconstbi  45277  sqrtnnaa  47857  sqrtnzqaa  47858  zlmodzxzscm  49413  nelsubclem  50119  aacllem  50883  veroquadmodzerod  50928