Theorem fconst 5724

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	|- B e. _V

Assertion

Ref	Expression
fconst	|- ( A X. { B } ) : A --> { B }

Proof of Theorem fconst

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fconst.1	. . 3 |- B e. _V
2		fconstmpt 4835	. . 3 |- ( A X. { B } ) = ( x e. A |-> B )
3	1, 2	fnmpti 5662	. 2 |- ( A X. { B } ) Fn A
4		rnxpss 5226	. 2 |- ran ( A X. { B } ) C_ { B }
5		df-f 5543	. 2 |- ( ( A X. { B } ) : A --> { B } <-> ( ( A X. { B } ) Fn A /\ ran ( A X. { B } ) C_ { B } ) )
6	3, 4, 5	mpbir2an 928	1 |- ( A X. { B } ) : A --> { B }

Syntax hints:   e. wcel 1872   _Vcvv 3017   C_ wss 3374   {csn 3936   X. cxp 4789   ran crn 4792   Fn wfn 5534   -->wf 5535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pr 4598

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-fun 5541  df-fn 5542  df-f 5543

This theorem is referenced by:  fconstg  5725  fodomr  7671  ofsubeq0  10552  ser0f  12211  hashgval  12463  hashinf  12465  hashf  12467  prodf1f  13886  pwssplit1  18220  psrbag0  18655  xkofvcn  20636  ibl0  22681  dvcmul  22835  dvcmulf  22836  dvexp  22844  elqaalem3  23211  elqaalem3OLD  23214  basellem7  23950  basellem9  23952  axlowdimlem8  24916  axlowdimlem9  24917  axlowdimlem10  24918  axlowdimlem11  24919  axlowdimlem12  24920  0oo  26367  occllem  26893  ho01i  27418  nlelchi  27651  hmopidmchi  27741  eulerpartlemt  29151  plymul02  29382  fullfunfnv  30657  fullfunfv  30658  poimirlem16  31863  poimirlem19  31866  poimirlem23  31870  poimirlem24  31871  poimirlem25  31872  poimirlem28  31875  poimirlem29  31876  poimirlem30  31877  poimirlem31  31878  poimirlem32  31879  ftc1anclem5  31928  lfl0f  32547  diophrw  35513  pwssplit4  35860  ofsubid  36586  dvsconst  36592  dvsid  36593  binomcxplemnn0  36611  binomcxplemnotnn0  36618  aacllem  40133