Theorem fconstmpt 5747

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 4642	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 623	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5210	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5691	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5226	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2775	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {csn 4626  {copab 5205   ↦ cmpt 5225   × cxp 5683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-sn 4627  df-opab 5206  df-mpt 5226  df-xp 5691

This theorem is referenced by:  fconst  6794  fcoconst  7154  fmptsn  7187  rnmptc  7227  fconstmpo  7550  ofc12  7727  caofinvl  7729  caofidlcan  7735  xpexgALT  8006  cantnf  9733  cnfcom2lem  9741  repsconst  14810  harmonic  15895  geomulcvg  15912  vdwlem8  17026  ramcl  17067  pwsvscafval  17539  setcepi  18133  diag2  18290  pws0g  18786  smndex1igid  18917  0frgp  19797  pwsgsum  20000  rrgsupp  20701  lmhmvsca  21044  uvcresum  21813  psrlinv  21975  psrlidm  21982  psrridm  21983  psrass23l  21987  psrass23  21989  mplcoe1  22055  mplcoe3  22056  mplcoe5  22058  mplmon2  22085  evlslem2  22103  evlslem1  22106  mhpsclcl  22151  psdmul  22170  psdmvr  22173  coe1z  22266  coe1mul2lem1  22270  coe1tm  22276  coe1sclmul  22285  coe1sclmul2  22287  evls1sca  22327  evl1sca  22338  evls1fpws  22373  grpvrinv  22403  mdetunilem9  22626  pttoponconst  23605  cnmptc  23670  cnmptkc  23687  pt1hmeo  23814  tmdgsum2  24104  tsms0  24150  tgptsmscls  24158  resspwsds  24382  imasdsf1olem  24383  nmoeq0  24757  idnghm  24764  rrxcph  25426  ovolctb  25525  ovoliunnul  25542  vitalilem4  25646  vitalilem5  25647  ismbf  25663  mbfconst  25668  mbfss  25681  mbfmulc2re  25683  mbfneg  25685  mbfmulc2  25698  itg11  25726  itg2const  25775  itg2mulclem  25781  itg2mulc  25782  itg2monolem1  25785  itg0  25815  itgz  25816  itgvallem3  25821  iblposlem  25827  i1fibl  25843  itgitg1  25844  itgge0  25846  iblconst  25853  itgconst  25854  itgfsum  25862  iblmulc2  25866  itgmulc2lem1  25867  bddmulibl  25874  bddiblnc  25877  dvcmulf  25982  dvexp  25991  dvexp2  25992  dvmptid  25995  dvmptc  25996  dvef  26018  rolle  26028  dv11cn  26040  ftc1lem4  26080  ftc2  26085  tdeglem4  26099  ply1nzb  26162  plyconst  26245  plyeq0lem  26249  plypf1  26251  coeeulem  26263  plyco  26280  0dgr  26284  0dgrb  26285  dgrcolem2  26314  dgrco  26315  plyremlem  26346  elqaalem3  26363  iaa  26367  taylply2  26409  taylply2OLD  26410  itgulm  26451  amgmlem  27033  lgam1  27107  ftalem7  27122  basellem8  27131  dchrfi  27299  dchrptlem3  27310  bra0  31969  padct  32731  cshw1s2  32945  fedgmullem2  33681  zar0ring  33877  xrge0mulc1cn  33940  esumnul  34049  esum0  34050  esumcvg  34087  ofcc  34107  mbfmcst  34261  sibf0  34336  0rrv  34453  ccatmulgnn0dir  34557  plymul02  34561  plymulx  34563  txsconnlem  35245  cvmliftphtlem  35322  faclim  35746  matunitlindflem1  37623  poimirlem30  37657  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  itg2addnclem  37678  iblmulc2nc  37692  itgmulc2nclem1  37693  itgmulc2nclem2  37694  itgmulc2nc  37695  itgabsnc  37696  ftc1cnnclem  37698  ftc1anclem3  37702  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc2nc  37709  repwsmet  37841  rrnequiv  37842  evlsvvval  42573  fsuppssindlem2  42602  fsuppssind  42603  mzpconstmpt  42751  mzpcompact2lem  42762  mendlmod  43201  mendassa  43202  mnringmulrcld  44247  expgrowthi  44352  expgrowth  44354  binomcxplemrat  44369  binomcxplemnotnn0  44375  climconstmpt  45673  iblconstmpt  45971  iblempty  45980  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  stoweidlem21  46036  lindsrng01  48385  eufsn  48751  aacllem  49320  amgmlemALT  49322