Theorem fconstmpt 5048

Description: Representation of a constant function using the mapping operation. (Note that cannot appear free in .) (Contributed by NM, 12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)

Assertion

Ref	Expression
fconstmpt

Distinct variable groups:   ,   ,

Proof of Theorem fconstmpt

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elsn 4043	. . . 4
2	1	anbi2i 694	. . 3
3	2	opabbii 4516	. 2
4		df-xp 5010	. 2
5		df-mpt 4512	. 2
6	3, 4, 5	3eqtr4i 2496	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  {csn 4029  {copab 4509  e.cmpt 4510  X.cxp 5002

This theorem is referenced by:  fconst  5776  fcoconst  6068  fmptsn  6091  fconstmpt2  6397  ofc12  6565  caofinvl  6567  xpexgALT  6793  cantnf  8133  cantnfOLD  8155  cnfcom2lem  8166  cnfcom2lemOLD  8174  repsconst  12744  harmonic  13670  geomulcvg  13685  vdwlem8  14506  ramcl  14547  pwsvscafval  14891  setcepi  15415  diag2  15514  pws0g  15956  0frgp  16797  pwsgsum  17009  pwsgsumOLD  17010  lmhmvsca  17691  rrgsupp  17939  rrgsuppOLD  17940  psrlinv  18050  psrlidm  18056  psrridm  18058  psrass23l  18063  psrass23  18065  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  mplmon2  18158  evlslem2  18180  evlslem1  18184  coe1z  18304  coe1mul2lem1  18308  coe1tm  18314  coe1sclmul  18323  coe1sclmul2  18325  evls1sca  18360  evl1sca  18370  uvcresum  18824  grpvrinv  18898  mdetunilem9  19122  pttoponconst  20098  cnmptc  20163  cnmptkc  20180  pt1hmeo  20307  tmdgsum2  20595  tsms0  20643  tgptsmscls  20652  resspwsds  20875  imasdsf1olem  20876  nmoeq0  21243  idnghm  21250  rrxcph  21824  ovolctb  21901  ovoliunnul  21918  vitalilem4  22020  vitalilem5  22021  ismbf  22037  mbfconst  22042  mbfss  22053  mbfmulc2re  22055  mbfneg  22057  mbfmulc2  22070  itg11  22098  itg2const  22147  itg2mulclem  22153  itg2mulc  22154  itg2monolem1  22157  itg0  22186  itgz  22187  itgvallem3  22192  iblposlem  22198  i1fibl  22214  itgitg1  22215  itgge0  22217  iblconst  22224  itgconst  22225  itgfsum  22233  iblmulc2  22237  itgmulc2lem1  22238  bddmulibl  22245  dvcmulf  22348  dvexp  22356  dvexp2  22357  dvmptid  22360  dvmptc  22361  dvef  22381  rolle  22391  dv11cn  22402  ftc1lem4  22440  ftc2  22445  tdeglem4  22458  ply1nzb  22523  plyconst  22603  plyeq0lem  22607  plypf1  22609  coeeulem  22621  plyco  22638  0dgr  22642  0dgrb  22643  dgrcolem2  22671  dgrco  22672  plyremlem  22700  elqaalem3  22717  iaa  22721  taylply2  22763  itgulm  22803  amgmlem  23319  ftalem7  23352  basellem8  23361  dchrfi  23530  dchrptlem3  23541  bra0  26869  xrge0mulc1cn  27923  esumnul  28059  esum0  28060  esumcvg  28092  ofcc  28105  mbfmcst  28230  sibf0  28276  0rrv  28390  ccatmulgnn0dir  28496  plymul02  28503  plymulx  28505  lgam1  28606  txsconlem  28685  cvmliftphtlem  28762  faclim  29171  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  itg2addnclem  30066  iblmulc2nc  30080  itgmulc2nclem1  30081  itgmulc2nclem2  30082  itgmulc2nc  30083  itgabsnc  30084  bddiblnc  30085  ftc1cnnclem  30088  ftc1anclem3  30092  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anclem8  30097  ftc2nc  30099  repwsmet  30330  rrnequiv  30331  mzpconstmpt  30672  mzpcompact2lem  30684  mendlmod  31142  mendassa  31143  expgrowthi  31238  expgrowth  31240  binomcxplemrat  31255  binomcxplemnotnn0  31261  rnmptc  31449  iblconstmpt  31754  iblempty  31764  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem21  31803  lindsrng01  33069  aacllem  33216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sn 4030  df-opab 4511  df-mpt 4512  df-xp 5010