Theorem fconst 5769

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 5042	. . 3 |- ( A X. { B } ) = ( x e. A |-> B )
3	1, 2	fnmpti 5707	. 2 |- ( A X. { B } ) Fn A
4		rnxpss 5437	. 2 |- ran ( A X. { B } ) C_ { B }
5		df-f 5590	. 2 |- ( ( A X. { B } ) : A --> { B } <-> ( ( A X. { B } ) Fn A /\ ran ( A X. { B } ) C_ { B } ) )
6	3, 4, 5	mpbir2an 918	1 |- ( A X. { B } ) : A --> { B }

Syntax hints:   e. wcel 1767   _Vcvv 3113   C_ wss 3476   {csn 4027   X. cxp 4997   ran crn 5000   Fn wfn 5581   -->wf 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-fun 5588  df-fn 5589  df-f 5590

This theorem is referenced by:  fconstg  5770  fodomr  7665  ofsubeq0  10529  ser0f  12124  hashgval  12372  hashinf  12374  hashf  12376  pwssplit1  17488  psrbag0  17930  xkofvcn  19920  ibl0  21928  dvcmul  22082  dvcmulf  22083  dvexp  22091  elqaalem3  22451  basellem7  23088  basellem9  23090  axlowdimlem8  23928  axlowdimlem9  23929  axlowdimlem10  23930  axlowdimlem11  23931  axlowdimlem12  23932  0oo  25380  occllem  25897  ho01i  26423  nlelchi  26656  hmopidmchi  26746  eulerpartlemt  27950  plymul02  28143  prodf1f  28603  fullfunfnv  29173  fullfunfv  29174  ftc1anclem5  29671  diophrw  30296  pwssplit4  30639  ofsubid  30829  dvsconst  30835  dvsid  30836  lfl0f  33866