Theorem fconst 6004

Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Hypothesis

Ref	Expression
fconst.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
fconst	⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵}

Proof of Theorem fconst

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fconst.1	. . 3 ⊢ 𝐵 ∈ V
2		fconstmpt 5085	. . 3 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fnmpti 5935	. 2 ⊢ (𝐴 × {𝐵}) Fn 𝐴
4		rnxpss 5485	. 2 ⊢ ran (𝐴 × {𝐵}) ⊆ {𝐵}
5		df-f 5808	. 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} ↔ ((𝐴 × {𝐵}) Fn 𝐴 ∧ ran (𝐴 × {𝐵}) ⊆ {𝐵}))
6	3, 4, 5	mpbir2an 957	1 ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵}

Syntax hints:   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  {csn 4125   × cxp 5036  ran crn 5039   Fn wfn 5799  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-fun 5806  df-fn 5807  df-f 5808

This theorem is referenced by:  fconstg  6005  fodomr  7996  ofsubeq0  10894  ser0f  12716  hashgval  12982  hashinf  12984  hashfxnn0  12986  hashfOLD  12988  prodf1f  14463  pwssplit1  18880  psrbag0  19315  xkofvcn  21297  ibl0  23359  dvcmul  23513  dvcmulf  23514  dvexp  23522  elqaalem3  23880  basellem7  24613  basellem9  24615  axlowdimlem8  25629  axlowdimlem9  25630  axlowdimlem10  25631  axlowdimlem11  25632  axlowdimlem12  25633  0oo  27028  occllem  27546  ho01i  28071  nlelchi  28304  hmopidmchi  28394  eulerpartlemt  29760  plymul02  29949  fullfunfnv  31223  fullfunfv  31224  poimirlem16  32595  poimirlem19  32598  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem28  32607  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  ftc1anclem5  32659  lfl0f  33374  diophrw  36340  pwssplit4  36677  ofsubid  37545  dvsconst  37551  dvsid  37552  binomcxplemnn0  37570  binomcxplemnotnn0  37577  aacllem  42356