Theorem fconst 6764

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

This proof depends on syntax axioms:   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904  {csn 4588   × cxp 5658  ran crn 5661   Fn wfn 6531  ⟶wf 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-fun 6538  df-fn 6539  df-f 6540

This theorem is used by:  fconstg  6765  fodomr  9114  fodomfir  9285  ofsubeq0  12221  ser0f  14098  hashgval  14376  hashinf  14378  hashfxnn0  14380  prodf1f  15953  pwssplit1  21191  psrbag0  22224  xkofvcn  23852  rrx0el  25568  ibl0  25957  dvcmul  26114  dvcmulf  26115  dvexp  26123  plymul02  26452  elqaalem3  26493  basellem7  27262  basellem9  27264  noetasuplem4  27911  axlowdimlem8  29310  axlowdimlem9  29311  axlowdimlem10  29312  axlowdimlem11  29313  axlowdimlem12  29314  0oo  31152  occllem  31666  ho01i  32191  nlelchi  32424  hmopidmchi  32514  elrgspnlem1  33571  gsumind  33674  esplyfval0  33963  eulerpartlemt  34770  breprexpnat  35030  fullfunfnv  36446  fullfunfv  36447  poimirlem16  38315  poimirlem19  38318  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem28  38327  poimirlem29  38328  poimirlem30  38329  poimirlem31  38330  poimirlem32  38331  ftc1anclem5  38376  lfl0f  39871  diophrw  43518  pwssplit4  43844  ofsubid  45062  dvsconst  45068  dvsid  45069  binomcxplemnn0  45087  binomcxplemnotnn0  45094  functermc  50314  aacllem  50649