Theorem fconst 6718

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  {csn 4568   × cxp 5620  ran crn 5623   Fn wfn 6485  ⟶wf 6486

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 5231  ax-pr 5368

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 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  fconstg  6719  fodomr  9057  fodomfir  9229  ofsubeq0  12143  ser0f  13979  hashgval  14257  hashinf  14259  hashfxnn0  14261  prodf1f  15816  pwssplit1  21013  psrbag0  22018  xkofvcn  23627  rrx0el  25343  ibl0  25732  dvcmul  25889  dvcmulf  25890  dvexp  25898  elqaalem3  26269  basellem7  27037  basellem9  27039  noetasuplem4  27688  axlowdimlem8  29006  axlowdimlem9  29007  axlowdimlem10  29008  axlowdimlem11  29009  axlowdimlem12  29010  0oo  30849  occllem  31363  ho01i  31888  nlelchi  32121  hmopidmchi  32211  elrgspnlem1  33308  gsumind  33410  esplyfval0  33713  eulerpartlemt  34521  plymul02  34696  breprexpnat  34784  fullfunfnv  36134  fullfunfv  36135  poimirlem16  37948  poimirlem19  37951  poimirlem23  37955  poimirlem24  37956  poimirlem25  37957  poimirlem28  37960  poimirlem29  37961  poimirlem30  37962  poimirlem31  37963  poimirlem32  37964  ftc1anclem5  38009  lfl0f  39506  diophrw  43190  pwssplit4  43520  ofsubid  44754  dvsconst  44760  dvsid  44761  binomcxplemnn0  44779  binomcxplemnotnn0  44786  functermc  49941  aacllem  50234