Theorem fconst 6715

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

Syntax hints:   ∈ wcel 2114  Vcvv 3427   ⊆ wss 3885  {csn 4557   × cxp 5618  ran crn 5621   Fn wfn 6482  ⟶wf 6483

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-fun 6489  df-fn 6490  df-f 6491

This theorem is referenced by:  fconstg  6716  fodomr  9055  fodomfir  9227  ofsubeq0  12145  ser0f  14006  hashgval  14284  hashinf  14286  hashfxnn0  14288  prodf1f  15846  pwssplit1  21043  psrbag0  22029  xkofvcn  23637  rrx0el  25353  ibl0  25742  dvcmul  25899  dvcmulf  25900  dvexp  25908  elqaalem3  26275  basellem7  27038  basellem9  27040  noetasuplem4  27688  axlowdimlem8  29006  axlowdimlem9  29007  axlowdimlem10  29008  axlowdimlem11  29009  axlowdimlem12  29010  0oo  30848  occllem  31362  ho01i  31887  nlelchi  32120  hmopidmchi  32210  elrgspnlem1  33291  gsumind  33393  esplyfval0  33696  eulerpartlemt  34503  plymul02  34678  breprexpnat  34766  fullfunfnv  36116  fullfunfv  36117  poimirlem16  37945  poimirlem19  37948  poimirlem23  37952  poimirlem24  37953  poimirlem25  37954  poimirlem28  37957  poimirlem29  37958  poimirlem30  37959  poimirlem31  37960  poimirlem32  37961  ftc1anclem5  38006  lfl0f  39503  diophrw  43179  pwssplit4  43505  ofsubid  44739  dvsconst  44745  dvsid  44746  binomcxplemnn0  44764  binomcxplemnotnn0  44771  functermc  49971  aacllem  50264