Theorem fconst 6746

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914  {csn 4589   × cxp 5636  ran crn 5639   Fn wfn 6506  ⟶wf 6507

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  fconstg  6747  fodomr  9092  fodomfir  9279  ofsubeq0  12183  ser0f  14020  hashgval  14298  hashinf  14300  hashfxnn0  14302  prodf1f  15858  pwssplit1  20966  psrbag0  21969  xkofvcn  23571  rrx0el  25298  ibl0  25688  dvcmul  25847  dvcmulf  25848  dvexp  25857  elqaalem3  26229  basellem7  26997  basellem9  26999  noetasuplem4  27648  axlowdimlem8  28876  axlowdimlem9  28877  axlowdimlem10  28878  axlowdimlem11  28879  axlowdimlem12  28880  0oo  30718  occllem  31232  ho01i  31757  nlelchi  31990  hmopidmchi  32080  elrgspnlem1  33193  eulerpartlemt  34362  plymul02  34537  breprexpnat  34625  fullfunfnv  35934  fullfunfv  35935  poimirlem16  37630  poimirlem19  37633  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem28  37642  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  ftc1anclem5  37691  lfl0f  39062  diophrw  42747  pwssplit4  43078  ofsubid  44313  dvsconst  44319  dvsid  44320  binomcxplemnn0  44338  binomcxplemnotnn0  44345  functermc  49497  aacllem  49790