Theorem fconst 6721

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

Syntax hints:   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902  {csn 4581   × cxp 5623  ran crn 5626   Fn wfn 6488  ⟶wf 6489

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 5242  ax-nul 5252  ax-pr 5378

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  fconstg  6722  fodomr  9060  fodomfir  9232  ofsubeq0  12146  ser0f  13982  hashgval  14260  hashinf  14262  hashfxnn0  14264  prodf1f  15819  pwssplit1  21015  psrbag0  22021  xkofvcn  23632  rrx0el  25358  ibl0  25748  dvcmul  25907  dvcmulf  25908  dvexp  25917  elqaalem3  26289  basellem7  27057  basellem9  27059  noetasuplem4  27708  axlowdimlem8  29005  axlowdimlem9  29006  axlowdimlem10  29007  axlowdimlem11  29008  axlowdimlem12  29009  0oo  30847  occllem  31361  ho01i  31886  nlelchi  32119  hmopidmchi  32209  elrgspnlem1  33305  gsumind  33407  esplyfval0  33703  eulerpartlemt  34509  plymul02  34684  breprexpnat  34772  fullfunfnv  36121  fullfunfv  36122  poimirlem16  37808  poimirlem19  37811  poimirlem23  37815  poimirlem24  37816  poimirlem25  37817  poimirlem28  37820  poimirlem29  37821  poimirlem30  37822  poimirlem31  37823  poimirlem32  37824  ftc1anclem5  37869  lfl0f  39366  diophrw  43037  pwssplit4  43367  ofsubid  44601  dvsconst  44607  dvsid  44608  binomcxplemnn0  44626  binomcxplemnotnn0  44633  functermc  49789  aacllem  50082