Theorem fconst 6539

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441   ⊆ wss 3881  {csn 4525   × cxp 5517  ran crn 5520   Fn wfn 6319  ⟶wf 6320

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328

This theorem is referenced by:  fconstg  6540  fodomr  8652  ofsubeq0  11622  ser0f  13419  hashgval  13689  hashinf  13691  hashfxnn0  13693  prodf1f  15240  pwssplit1  19824  psrbag0  20733  xkofvcn  22289  rrx0el  24002  ibl0  24390  dvcmul  24547  dvcmulf  24548  dvexp  24556  elqaalem3  24917  basellem7  25672  basellem9  25674  axlowdimlem8  26743  axlowdimlem9  26744  axlowdimlem10  26745  axlowdimlem11  26746  axlowdimlem12  26747  0oo  28572  occllem  29086  ho01i  29611  nlelchi  29844  hmopidmchi  29934  eulerpartlemt  31739  plymul02  31926  breprexpnat  32015  noetalem3  33332  fullfunfnv  33520  fullfunfv  33521  poimirlem16  35073  poimirlem19  35076  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem28  35085  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  ftc1anclem5  35134  lfl0f  36365  diophrw  39700  pwssplit4  40033  ofsubid  41028  dvsconst  41034  dvsid  41035  binomcxplemnn0  41053  binomcxplemnotnn0  41060  aacllem  45329