Theorem fconst 6807

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  {csn 4648   × cxp 5698  ran crn 5701   Fn wfn 6568  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-fun 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  fconstg  6808  fodomr  9194  fodomfir  9396  ofsubeq0  12290  ser0f  14106  hashgval  14382  hashinf  14384  hashfxnn0  14386  prodf1f  15940  pwssplit1  21081  psrbag0  22109  xkofvcn  23713  rrx0el  25451  ibl0  25842  dvcmul  26001  dvcmulf  26002  dvexp  26011  elqaalem3  26381  basellem7  27148  basellem9  27150  noetasuplem4  27799  axlowdimlem8  28982  axlowdimlem9  28983  axlowdimlem10  28984  axlowdimlem11  28985  axlowdimlem12  28986  0oo  30821  occllem  31335  ho01i  31860  nlelchi  32093  hmopidmchi  32183  eulerpartlemt  34336  plymul02  34523  breprexpnat  34611  fullfunfnv  35910  fullfunfv  35911  poimirlem16  37596  poimirlem19  37599  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem28  37608  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  ftc1anclem5  37657  lfl0f  39025  diophrw  42715  pwssplit4  43046  ofsubid  44293  dvsconst  44299  dvsid  44300  binomcxplemnn0  44318  binomcxplemnotnn0  44325  aacllem  48895