Theorem fconstmpt 5640

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		velsn 4574	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 622	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5137	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5586	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5154	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2776	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {csn 4558  {copab 5132   ↦ cmpt 5153   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-sn 4559  df-opab 5133  df-mpt 5154  df-xp 5586

This theorem is referenced by:  fconst  6644  fcoconst  6988  fmptsn  7021  rnmptc  7064  rnmptcOLD  7065  fconstmpo  7369  ofc12  7539  caofinvl  7541  xpexgALT  7797  cantnf  9381  cnfcom2lem  9389  repsconst  14413  harmonic  15499  geomulcvg  15516  vdwlem8  16617  ramcl  16658  pwsvscafval  17122  setcepi  17719  diag2  17879  pws0g  18336  smndex1igid  18458  0frgp  19300  pwsgsum  19498  lmhmvsca  20222  rrgsupp  20475  uvcresum  20910  psrlinv  21076  psrlidm  21082  psrridm  21083  psrass23l  21087  psrass23  21089  mplcoe1  21148  mplcoe3  21149  mplcoe5  21151  mplmon2  21179  evlslem2  21199  evlslem1  21202  mhpsclcl  21247  coe1z  21344  coe1mul2lem1  21348  coe1tm  21354  coe1sclmul  21363  coe1sclmul2  21365  evls1sca  21399  evl1sca  21410  grpvrinv  21455  mdetunilem9  21677  pttoponconst  22656  cnmptc  22721  cnmptkc  22738  pt1hmeo  22865  tmdgsum2  23155  tsms0  23201  tgptsmscls  23209  resspwsds  23433  imasdsf1olem  23434  nmoeq0  23806  idnghm  23813  rrxcph  24461  ovolctb  24559  ovoliunnul  24576  vitalilem4  24680  vitalilem5  24681  ismbf  24697  mbfconst  24702  mbfss  24715  mbfmulc2re  24717  mbfneg  24719  mbfmulc2  24732  itg11  24760  itg2const  24810  itg2mulclem  24816  itg2mulc  24817  itg2monolem1  24820  itg0  24849  itgz  24850  itgvallem3  24855  iblposlem  24861  i1fibl  24877  itgitg1  24878  itgge0  24880  iblconst  24887  itgconst  24888  itgfsum  24896  iblmulc2  24900  itgmulc2lem1  24901  bddmulibl  24908  bddiblnc  24911  dvcmulf  25014  dvexp  25022  dvexp2  25023  dvmptid  25026  dvmptc  25027  dvef  25049  rolle  25059  dv11cn  25070  ftc1lem4  25108  ftc2  25113  tdeglem4  25129  tdeglem4OLD  25130  ply1nzb  25192  plyconst  25272  plyeq0lem  25276  plypf1  25278  coeeulem  25290  plyco  25307  0dgr  25311  0dgrb  25312  dgrcolem2  25340  dgrco  25341  plyremlem  25369  elqaalem3  25386  iaa  25390  taylply2  25432  itgulm  25472  amgmlem  26044  lgam1  26118  ftalem7  26133  basellem8  26142  dchrfi  26308  dchrptlem3  26319  bra0  30213  padct  30956  cshw1s2  31134  fedgmullem2  31613  zar0ring  31730  xrge0mulc1cn  31793  esumnul  31916  esum0  31917  esumcvg  31954  ofcc  31974  mbfmcst  32126  sibf0  32201  0rrv  32318  ccatmulgnn0dir  32421  plymul02  32425  plymulx  32427  txsconnlem  33102  cvmliftphtlem  33179  faclim  33618  matunitlindflem1  35700  poimirlem30  35734  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  itg2addnclem  35755  iblmulc2nc  35769  itgmulc2nclem1  35770  itgmulc2nclem2  35771  itgmulc2nc  35772  itgabsnc  35773  ftc1cnnclem  35775  ftc1anclem3  35779  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anclem8  35784  ftc2nc  35786  repwsmet  35919  rrnequiv  35920  evlsbagval  40198  fsuppssindlem2  40204  fsuppssind  40205  mzpconstmpt  40478  mzpcompact2lem  40489  mendlmod  40934  mendassa  40935  mnringmulrcld  41735  expgrowthi  41840  expgrowth  41842  binomcxplemrat  41857  binomcxplemnotnn0  41863  climconstmpt  43089  iblconstmpt  43387  iblempty  43396  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  stoweidlem21  43452  lindsrng01  45697  eufsn  46057  aacllem  46391  amgmlemALT  46393