Theorem fconstmpt 5681

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 4572	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 629	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5140	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5625	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5155	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2772	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {csn 4556  {copab 5135   ↦ cmpt 5154   × cxp 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-sn 4557  df-opab 5136  df-mpt 5155  df-xp 5625

This theorem is referenced by:  fconst  6714  fcoconst  7077  fmptsn  7112  rnmptc  7152  fconstmpo  7474  ofc12  7651  caofinvl  7653  caofidlcan  7659  xpexgALT  7924  cantnf  9606  cnfcom2lem  9614  repsconst  14726  harmonic  15816  geomulcvg  15833  vdwlem8  16951  ramcl  16992  pwsvscafval  17450  setcepi  18047  diag2  18203  pws0g  18733  smndex1gbas  18862  smndex1gid  18864  smndex1igid  18866  smndex1igidOLD  18867  0frgp  19746  pwsgsum  19949  rrgsupp  20674  lmhmvsca  21036  uvcresum  21769  psrlinv  21931  psrlidm  21937  psrridm  21938  psrass23l  21942  psrass23  21944  mplcoe1  22014  mplcoe3  22015  mplcoe5  22017  mplmon2  22038  evlslem2  22056  evlslem1  22059  evlsvvval  22070  mhpsclcl  22136  psdmul  22155  psdmvr  22158  coe1z  22250  coe1mul2lem1  22254  coe1tm  22260  coe1sclmul  22269  coe1sclmul2  22271  evls1sca  22310  evl1sca  22321  evls1fpws  22356  grpvrinv  22383  mdetunilem9  22604  pttoponconst  23581  cnmptc  23646  cnmptkc  23663  pt1hmeo  23790  tmdgsum2  24080  tsms0  24126  tgptsmscls  24134  resspwsds  24356  imasdsf1olem  24357  nmoeq0  24720  idnghm  24727  rrxcph  25378  ovolctb  25476  ovoliunnul  25493  vitalilem4  25597  vitalilem5  25598  ismbf  25614  mbfconst  25619  mbfss  25632  mbfmulc2re  25634  mbfneg  25636  mbfmulc2  25649  itg11  25677  itg2const  25726  itg2mulclem  25732  itg2mulc  25733  itg2monolem1  25736  itg0  25766  itgz  25767  itgvallem3  25772  iblposlem  25778  i1fibl  25794  itgitg1  25795  itgge0  25797  iblconst  25804  itgconst  25805  itgfsum  25813  iblmulc2  25817  itgmulc2lem1  25818  bddmulibl  25825  bddiblnc  25828  dvcmulf  25931  dvexp  25939  dvexp2  25940  dvmptid  25943  dvmptc  25944  dvef  25966  rolle  25976  dv11cn  25987  ftc1lem4  26025  ftc2  26030  tdeglem4  26044  ply1nzb  26107  plyconst  26190  plyeq0lem  26194  plypf1  26196  coeeulem  26208  plyco  26225  0dgr  26229  0dgrb  26230  dgrcolem2  26258  dgrco  26259  plyremlem  26289  elqaalem3  26306  iaa  26310  taylply2  26352  itgulm  26392  amgmlem  26972  lgam1  27046  ftalem7  27061  basellem8  27070  dchrfi  27237  dchrptlem3  27248  istrkg2ld  28547  bra0  32040  padct  32811  cshw1s2  33040  gsumind  33429  mplasclco  33709  selvply1rhmlem2  33714  selvply1rhm0  33719  extvfvcl  33729  mplvrpmmhm  33739  psrgsum  33741  psrmonprod  33745  esplyfval3  33765  fedgmullem2  33823  extdgfialglem2  33886  zar0ring  34071  xrge0mulc1cn  34134  esumnul  34241  esum0  34242  esumcvg  34279  ofcc  34299  mbfmcst  34452  sibf0  34527  0rrv  34644  ccatmulgnn0dir  34735  plymul02  34739  plymulx  34741  txsconnlem  35477  cvmliftphtlem  35554  faclim  35983  matunitlindflem1  37992  poimirlem30  38026  ovoliunnfl  38038  voliunnfl  38040  volsupnfl  38041  itg2addnclem  38047  iblmulc2nc  38061  itgmulc2nclem1  38062  itgmulc2nclem2  38063  itgmulc2nc  38064  itgabsnc  38065  ftc1cnnclem  38067  ftc1anclem3  38071  ftc1anclem5  38073  ftc1anclem7  38075  ftc1anclem8  38076  ftc2nc  38078  repwsmet  38210  rrnequiv  38211  fsuppssindlem2  43051  fsuppssind  43052  mzpconstmpt  43198  mzpcompact2lem  43209  mendlmod  43643  mendassa  43644  mnringmulrcld  44681  expgrowthi  44786  expgrowth  44788  binomcxplemrat  44803  binomcxplemnotnn0  44809  climconstmpt  46109  iblconstmpt  46407  iblempty  46416  itgiccshift  46431  itgperiod  46432  itgsbtaddcnst  46433  stoweidlem21  46472  hoicvr  46999  nthrucw  47339  cjnpoly  47360  lindsrng01  48967  eufsn  49340  diag1a  49803  aacllem  50299  amgmlemALT  50301