Theorem fconst 6795

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478   ⊆ wss 3963  {csn 4631   × cxp 5687  ran crn 5690   Fn wfn 6558  ⟶wf 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-fun 6565  df-fn 6566  df-f 6567

This theorem is referenced by:  fconstg  6796  fodomr  9167  fodomfir  9366  ofsubeq0  12261  ser0f  14093  hashgval  14369  hashinf  14371  hashfxnn0  14373  prodf1f  15925  pwssplit1  21076  psrbag0  22104  xkofvcn  23708  rrx0el  25446  ibl0  25837  dvcmul  25996  dvcmulf  25997  dvexp  26006  elqaalem3  26378  basellem7  27145  basellem9  27147  noetasuplem4  27796  axlowdimlem8  28979  axlowdimlem9  28980  axlowdimlem10  28981  axlowdimlem11  28982  axlowdimlem12  28983  0oo  30818  occllem  31332  ho01i  31857  nlelchi  32090  hmopidmchi  32180  elrgspnlem1  33232  eulerpartlemt  34353  plymul02  34540  breprexpnat  34628  fullfunfnv  35928  fullfunfv  35929  poimirlem16  37623  poimirlem19  37626  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem28  37635  poimirlem29  37636  poimirlem30  37637  poimirlem31  37638  poimirlem32  37639  ftc1anclem5  37684  lfl0f  39051  diophrw  42747  pwssplit4  43078  ofsubid  44320  dvsconst  44326  dvsid  44327  binomcxplemnn0  44345  binomcxplemnotnn0  44352  aacllem  49032