Theorem fconst 6774

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3947  {csn 4627   × cxp 5673  ran crn 5676   Fn wfn 6535  ⟶wf 6536

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-fun 6542  df-fn 6543  df-f 6544

This theorem is referenced by:  fconstg  6775  fodomr  9124  ofsubeq0  12205  ser0f  14017  hashgval  14289  hashinf  14291  hashfxnn0  14293  prodf1f  15834  pwssplit1  20662  psrbag0  21614  xkofvcn  23179  rrx0el  24906  ibl0  25295  dvcmul  25452  dvcmulf  25453  dvexp  25461  elqaalem3  25825  basellem7  26580  basellem9  26582  noetasuplem4  27228  axlowdimlem8  28196  axlowdimlem9  28197  axlowdimlem10  28198  axlowdimlem11  28199  axlowdimlem12  28200  0oo  30029  occllem  30543  ho01i  31068  nlelchi  31301  hmopidmchi  31391  eulerpartlemt  33358  plymul02  33545  breprexpnat  33634  fullfunfnv  34906  fullfunfv  34907  poimirlem16  36492  poimirlem19  36495  poimirlem23  36499  poimirlem24  36500  poimirlem25  36501  poimirlem28  36504  poimirlem29  36505  poimirlem30  36506  poimirlem31  36507  poimirlem32  36508  ftc1anclem5  36553  lfl0f  37927  diophrw  41482  pwssplit4  41816  ofsubid  43068  dvsconst  43074  dvsid  43075  binomcxplemnn0  43093  binomcxplemnotnn0  43100  aacllem  47801