Theorem fconstmpt 5739

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 4645	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 621	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5215	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5683	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5232	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2763	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 394   = wceq 1533   ∈ wcel 2098  {csn 4629  {copab 5210   ↦ cmpt 5231   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465  df-sn 4630  df-opab 5211  df-mpt 5232  df-xp 5683

This theorem is referenced by:  fconst  6781  fcoconst  7141  fmptsn  7174  rnmptc  7217  fconstmpo  7535  ofc12  7712  caofinvl  7714  xpexgALT  7984  cantnf  9716  cnfcom2lem  9724  repsconst  14754  harmonic  15837  geomulcvg  15854  vdwlem8  16956  ramcl  16997  pwsvscafval  17475  setcepi  18076  diag2  18236  pws0g  18729  smndex1igid  18860  0frgp  19738  pwsgsum  19941  lmhmvsca  20934  rrgsupp  21242  uvcresum  21731  psrlinv  21904  psrlidm  21911  psrridm  21912  psrass23l  21916  psrass23  21918  mplcoe1  21982  mplcoe3  21983  mplcoe5  21985  mplmon2  22012  evlslem2  22032  evlslem1  22035  mhpsclcl  22079  psdmul  22098  coe1z  22191  coe1mul2lem1  22195  coe1tm  22201  coe1sclmul  22210  coe1sclmul2  22212  evls1sca  22251  evl1sca  22262  evls1fpws  22297  grpvrinv  22329  mdetunilem9  22552  pttoponconst  23531  cnmptc  23596  cnmptkc  23613  pt1hmeo  23740  tmdgsum2  24030  tsms0  24076  tgptsmscls  24084  resspwsds  24308  imasdsf1olem  24309  nmoeq0  24683  idnghm  24690  rrxcph  25350  ovolctb  25449  ovoliunnul  25466  vitalilem4  25570  vitalilem5  25571  ismbf  25587  mbfconst  25592  mbfss  25605  mbfmulc2re  25607  mbfneg  25609  mbfmulc2  25622  itg11  25650  itg2const  25700  itg2mulclem  25706  itg2mulc  25707  itg2monolem1  25710  itg0  25739  itgz  25740  itgvallem3  25745  iblposlem  25751  i1fibl  25767  itgitg1  25768  itgge0  25770  iblconst  25777  itgconst  25778  itgfsum  25786  iblmulc2  25790  itgmulc2lem1  25791  bddmulibl  25798  bddiblnc  25801  dvcmulf  25906  dvexp  25915  dvexp2  25916  dvmptid  25919  dvmptc  25920  dvef  25942  rolle  25952  dv11cn  25964  ftc1lem4  26004  ftc2  26009  tdeglem4  26025  tdeglem4OLD  26026  ply1nzb  26088  plyconst  26170  plyeq0lem  26174  plypf1  26176  coeeulem  26188  plyco  26205  0dgr  26209  0dgrb  26210  dgrcolem2  26239  dgrco  26240  plyremlem  26269  elqaalem3  26286  iaa  26290  taylply2  26332  taylply2OLD  26333  itgulm  26374  amgmlem  26952  lgam1  27026  ftalem7  27041  basellem8  27050  dchrfi  27218  dchrptlem3  27229  bra0  31816  padct  32558  cshw1s2  32738  fedgmullem2  33398  zar0ring  33549  xrge0mulc1cn  33612  esumnul  33737  esum0  33738  esumcvg  33775  ofcc  33795  mbfmcst  33949  sibf0  34024  0rrv  34141  ccatmulgnn0dir  34244  plymul02  34248  plymulx  34250  txsconnlem  34920  cvmliftphtlem  34997  faclim  35410  matunitlindflem1  37159  poimirlem30  37193  ovoliunnfl  37205  voliunnfl  37207  volsupnfl  37208  itg2addnclem  37214  iblmulc2nc  37228  itgmulc2nclem1  37229  itgmulc2nclem2  37230  itgmulc2nc  37231  itgabsnc  37232  ftc1cnnclem  37234  ftc1anclem3  37238  ftc1anclem5  37240  ftc1anclem7  37242  ftc1anclem8  37243  ftc2nc  37245  repwsmet  37377  rrnequiv  37378  evlsvvval  41861  fsuppssindlem2  41890  fsuppssind  41891  mzpconstmpt  42225  mzpcompact2lem  42236  mendlmod  42682  mendassa  42683  mnringmulrcld  43730  expgrowthi  43835  expgrowth  43837  binomcxplemrat  43852  binomcxplemnotnn0  43858  climconstmpt  45109  iblconstmpt  45407  iblempty  45416  itgiccshift  45431  itgperiod  45432  itgsbtaddcnst  45433  stoweidlem21  45472  lindsrng01  47648  eufsn  48006  aacllem  48346  amgmlemALT  48348