Theorem fconst 6750

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3905  {csn 4583   × cxp 5646  ran crn 5649   Fn wfn 6516  ⟶wf 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-fun 6523  df-fn 6524  df-f 6525

This theorem is referenced by:  fconstg  6751  fodomr  9100  fodomfir  9271  ofsubeq0  12202  ser0f  14078  hashgval  14356  hashinf  14358  hashfxnn0  14360  prodf1f  15932  pwssplit1  21133  psrbag0  22122  xkofvcn  23751  rrx0el  25467  ibl0  25856  dvcmul  26013  dvcmulf  26014  dvexp  26022  plymul02  26351  elqaalem3  26392  basellem7  27158  basellem9  27160  noetasuplem4  27807  axlowdimlem8  29157  axlowdimlem9  29158  axlowdimlem10  29159  axlowdimlem11  29160  axlowdimlem12  29161  0oo  30999  occllem  31513  ho01i  32038  nlelchi  32271  hmopidmchi  32361  elrgspnlem1  33429  gsumind  33534  esplyfval0  33863  eulerpartlemt  34670  breprexpnat  34930  fullfunfnv  36301  fullfunfv  36302  poimirlem16  38140  poimirlem19  38143  poimirlem23  38147  poimirlem24  38148  poimirlem25  38149  poimirlem28  38152  poimirlem29  38153  poimirlem30  38154  poimirlem31  38155  poimirlem32  38156  ftc1anclem5  38201  lfl0f  39698  diophrw  43345  pwssplit4  43671  ofsubid  44891  dvsconst  44897  dvsid  44898  binomcxplemnn0  44916  binomcxplemnotnn0  44923  functermc  50120  aacllem  50413