Theorem fnconstg 6131

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 6130	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		ffn 6083	. 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} → (𝐴 × {𝐵}) Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2030  {csn 4210   × cxp 5141   Fn wfn 5921  ⟶wf 5922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-fun 5928  df-fn 5929  df-f 5930

This theorem is referenced by:  fconst2g  6509  ofc1  6962  ofc2  6963  caofid0l  6967  caofid0r  6968  caofid1  6969  caofid2  6970  fnsuppres  7367  fczsupp0  7369  fczfsuppd  8334  brwdom2  8519  cantnf0  8610  ofnegsub  11056  ofsubge0  11057  pwsplusgval  16197  pwsmulrval  16198  pwsvscafval  16201  xpsc0  16267  xpsc1  16268  pwsco1mhm  17417  dprdsubg  18469  pwsmgp  18664  pwssplit1  19107  frlmpwsfi  20144  frlmbas  20147  frlmvscaval  20158  islindf4  20225  tmdgsum2  21947  0plef  23484  0pledm  23485  itg1ge0  23498  mbfi1fseqlem5  23531  xrge0f  23543  itg2ge0  23547  itg2addlem  23570  bddibl  23651  dvidlem  23724  rolle  23798  dveq0  23808  dv11cn  23809  tdeglem4  23865  mdeg0  23875  fta1blem  23973  qaa  24123  basellem9  24860  ofcc  30296  ofcof  30297  eulerpartlemt  30561  noextendseq  31945  matunitlindflem1  33535  matunitlindflem2  33536  ptrecube  33539  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  poimirlem32  33571  broucube  33573  cnpwstotbnd  33726  eqlkr2  34705  pwssplit4  37976  mpaaeu  38037  rngunsnply  38060  ofdivrec  38842  dvconstbi  38850  zlmodzxzscm  42460  aacllem  42875