Theorem fconst 6727

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 5693	. . 3 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fnmpti 6642	. 2 ⊢ (𝐴 × {𝐵}) Fn 𝐴
4		rnxpss 6137	. 2 ⊢ ran (𝐴 × {𝐵}) ⊆ {𝐵}
5		df-f 6503	. 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} ↔ ((𝐴 × {𝐵}) Fn 𝐴 ∧ ran (𝐴 × {𝐵}) ⊆ {𝐵}))
6	3, 4, 5	mpbir2an 712	1 ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵}

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  {csn 4568   × cxp 5629  ran crn 5632   Fn wfn 6494  ⟶wf 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6501  df-fn 6502  df-f 6503

This theorem is referenced by:  fconstg  6728  fodomr  9066  fodomfir  9238  ofsubeq0  12156  ser0f  14017  hashgval  14295  hashinf  14297  hashfxnn0  14299  prodf1f  15857  pwssplit1  21054  psrbag0  22040  xkofvcn  23649  rrx0el  25365  ibl0  25754  dvcmul  25911  dvcmulf  25912  dvexp  25920  elqaalem3  26287  basellem7  27050  basellem9  27052  noetasuplem4  27700  axlowdimlem8  29018  axlowdimlem9  29019  axlowdimlem10  29020  axlowdimlem11  29021  axlowdimlem12  29022  0oo  30860  occllem  31374  ho01i  31899  nlelchi  32132  hmopidmchi  32222  elrgspnlem1  33303  gsumind  33405  esplyfval0  33708  eulerpartlemt  34515  plymul02  34690  breprexpnat  34778  fullfunfnv  36128  fullfunfv  36129  poimirlem16  37957  poimirlem19  37960  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem28  37969  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  ftc1anclem5  38018  lfl0f  39515  diophrw  43191  pwssplit4  43517  ofsubid  44751  dvsconst  44757  dvsid  44758  binomcxplemnn0  44776  binomcxplemnotnn0  44783  functermc  49977  aacllem  50270