Theorem fconst 6735

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

Syntax hints:   ∈ wcel 2132  Vcvv 3444   ⊆ wss 3895  {csn 4572   × cxp 5634  ran crn 5637   Fn wfn 6501  ⟶wf 6502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-fun 6508  df-fn 6509  df-f 6510

This theorem is referenced by:  fconstg  6736  fodomr  9085  fodomfir  9257  ofsubeq0  12178  ser0f  14054  hashgval  14332  hashinf  14334  hashfxnn0  14336  prodf1f  15894  pwssplit1  21095  psrbag0  22084  xkofvcn  23713  rrx0el  25429  ibl0  25818  dvcmul  25975  dvcmulf  25976  dvexp  25984  elqaalem3  26351  basellem7  27117  basellem9  27119  noetasuplem4  27766  axlowdimlem8  29085  axlowdimlem9  29086  axlowdimlem10  29087  axlowdimlem11  29088  axlowdimlem12  29089  0oo  30927  occllem  31441  ho01i  31966  nlelchi  32199  hmopidmchi  32289  elrgspnlem1  33372  gsumind  33477  esplyfval0  33805  eulerpartlemt  34612  plymul02  34787  breprexpnat  34875  fullfunfnv  36234  fullfunfv  36235  poimirlem16  38073  poimirlem19  38076  poimirlem23  38080  poimirlem24  38081  poimirlem25  38082  poimirlem28  38085  poimirlem29  38086  poimirlem30  38087  poimirlem31  38088  poimirlem32  38089  ftc1anclem5  38134  lfl0f  39631  diophrw  43278  pwssplit4  43604  ofsubid  44838  dvsconst  44844  dvsid  44845  binomcxplemnn0  44863  binomcxplemnotnn0  44870  functermc  50067  aacllem  50360