Theorem fconst 6748

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3916  {csn 4591   × cxp 5638  ran crn 5641   Fn wfn 6508  ⟶wf 6509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-fun 6515  df-fn 6516  df-f 6517

This theorem is referenced by:  fconstg  6749  fodomr  9097  fodomfir  9285  ofsubeq0  12184  ser0f  14026  hashgval  14304  hashinf  14306  hashfxnn0  14308  prodf1f  15864  pwssplit1  20972  psrbag0  21975  xkofvcn  23577  rrx0el  25304  ibl0  25694  dvcmul  25853  dvcmulf  25854  dvexp  25863  elqaalem3  26235  basellem7  27003  basellem9  27005  noetasuplem4  27654  axlowdimlem8  28882  axlowdimlem9  28883  axlowdimlem10  28884  axlowdimlem11  28885  axlowdimlem12  28886  0oo  30724  occllem  31238  ho01i  31763  nlelchi  31996  hmopidmchi  32086  elrgspnlem1  33199  eulerpartlemt  34368  plymul02  34543  breprexpnat  34631  fullfunfnv  35929  fullfunfv  35930  poimirlem16  37625  poimirlem19  37628  poimirlem23  37632  poimirlem24  37633  poimirlem25  37634  poimirlem28  37637  poimirlem29  37638  poimirlem30  37639  poimirlem31  37640  poimirlem32  37641  ftc1anclem5  37686  lfl0f  39057  diophrw  42740  pwssplit4  43071  ofsubid  44306  dvsconst  44312  dvsid  44313  binomcxplemnn0  44331  binomcxplemnotnn0  44338  functermc  49487  aacllem  49780