Theorem fconst 6788

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

Syntax hints:   ∈ wcel 2098  Vcvv 3473   ⊆ wss 3949  {csn 4632   × cxp 5680  ran crn 5683   Fn wfn 6548  ⟶wf 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-fun 6555  df-fn 6556  df-f 6557

This theorem is referenced by:  fconstg  6789  fodomr  9159  ofsubeq0  12247  ser0f  14060  hashgval  14332  hashinf  14334  hashfxnn0  14336  prodf1f  15878  pwssplit1  20951  psrbag0  22013  xkofvcn  23608  rrx0el  25346  ibl0  25736  dvcmul  25895  dvcmulf  25896  dvexp  25905  elqaalem3  26276  basellem7  27039  basellem9  27041  noetasuplem4  27689  axlowdimlem8  28780  axlowdimlem9  28781  axlowdimlem10  28782  axlowdimlem11  28783  axlowdimlem12  28784  0oo  30619  occllem  31133  ho01i  31658  nlelchi  31891  hmopidmchi  31981  eulerpartlemt  34024  plymul02  34211  breprexpnat  34299  fullfunfnv  35575  fullfunfv  35576  poimirlem16  37142  poimirlem19  37145  poimirlem23  37149  poimirlem24  37150  poimirlem25  37151  poimirlem28  37154  poimirlem29  37155  poimirlem30  37156  poimirlem31  37157  poimirlem32  37158  ftc1anclem5  37203  lfl0f  38573  diophrw  42210  pwssplit4  42544  ofsubid  43792  dvsconst  43798  dvsid  43799  binomcxplemnn0  43817  binomcxplemnotnn0  43824  aacllem  48312