Theorem fconst 6715

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897  {csn 4575   × cxp 5617  ran crn 5620   Fn wfn 6482  ⟶wf 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6489  df-fn 6490  df-f 6491

This theorem is referenced by:  fconstg  6716  fodomr  9047  fodomfir  9218  ofsubeq0  12128  ser0f  13968  hashgval  14246  hashinf  14248  hashfxnn0  14250  prodf1f  15805  pwssplit1  20999  psrbag0  22003  xkofvcn  23605  rrx0el  25331  ibl0  25721  dvcmul  25880  dvcmulf  25881  dvexp  25890  elqaalem3  26262  basellem7  27030  basellem9  27032  noetasuplem4  27681  axlowdimlem8  28934  axlowdimlem9  28935  axlowdimlem10  28936  axlowdimlem11  28937  axlowdimlem12  28938  0oo  30776  occllem  31290  ho01i  31815  nlelchi  32048  hmopidmchi  32138  elrgspnlem1  33216  gsumind  33317  eulerpartlemt  34391  plymul02  34566  breprexpnat  34654  fullfunfnv  35997  fullfunfv  35998  poimirlem16  37682  poimirlem19  37685  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem28  37694  poimirlem29  37695  poimirlem30  37696  poimirlem31  37697  poimirlem32  37698  ftc1anclem5  37743  lfl0f  39174  diophrw  42857  pwssplit4  43187  ofsubid  44422  dvsconst  44428  dvsid  44429  binomcxplemnn0  44447  binomcxplemnotnn0  44454  functermc  49614  aacllem  49907