Theorem fconst 6793

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

Syntax hints:   ∈ wcel 2107  Vcvv 3479   ⊆ wss 3950  {csn 4625   × cxp 5682  ran crn 5685   Fn wfn 6555  ⟶wf 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-fun 6562  df-fn 6563  df-f 6564

This theorem is referenced by:  fconstg  6794  fodomr  9169  fodomfir  9369  ofsubeq0  12264  ser0f  14097  hashgval  14373  hashinf  14375  hashfxnn0  14377  prodf1f  15929  pwssplit1  21059  psrbag0  22087  xkofvcn  23693  rrx0el  25433  ibl0  25823  dvcmul  25982  dvcmulf  25983  dvexp  25992  elqaalem3  26364  basellem7  27131  basellem9  27133  noetasuplem4  27782  axlowdimlem8  28965  axlowdimlem9  28966  axlowdimlem10  28967  axlowdimlem11  28968  axlowdimlem12  28969  0oo  30809  occllem  31323  ho01i  31848  nlelchi  32081  hmopidmchi  32171  elrgspnlem1  33247  eulerpartlemt  34374  plymul02  34562  breprexpnat  34650  fullfunfnv  35948  fullfunfv  35949  poimirlem16  37644  poimirlem19  37647  poimirlem23  37651  poimirlem24  37652  poimirlem25  37653  poimirlem28  37656  poimirlem29  37657  poimirlem30  37658  poimirlem31  37659  poimirlem32  37660  ftc1anclem5  37705  lfl0f  39071  diophrw  42775  pwssplit4  43106  ofsubid  44348  dvsconst  44354  dvsid  44355  binomcxplemnn0  44373  binomcxplemnotnn0  44380  functermc  49168  aacllem  49375