Theorem fconstmpt 5738

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

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {csn 4628  {copab 5210   ↦ cmpt 5231   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-sn 4629  df-opab 5211  df-mpt 5232  df-xp 5682

This theorem is referenced by:  fconst  6777  fcoconst  7134  fmptsn  7167  rnmptc  7210  rnmptcOLD  7211  fconstmpo  7527  ofc12  7700  caofinvl  7702  xpexgALT  7970  cantnf  9690  cnfcom2lem  9698  repsconst  14724  harmonic  15807  geomulcvg  15824  vdwlem8  16923  ramcl  16964  pwsvscafval  17442  setcepi  18040  diag2  18200  pws0g  18663  smndex1igid  18787  0frgp  19649  pwsgsum  19852  lmhmvsca  20661  rrgsupp  20913  uvcresum  21354  psrlinv  21522  psrlidm  21529  psrridm  21530  psrass23l  21534  psrass23  21536  mplcoe1  21598  mplcoe3  21599  mplcoe5  21601  mplmon2  21628  evlslem2  21648  evlslem1  21651  mhpsclcl  21696  coe1z  21792  coe1mul2lem1  21796  coe1tm  21802  coe1sclmul  21811  coe1sclmul2  21813  evls1sca  21849  evl1sca  21860  grpvrinv  21905  mdetunilem9  22129  pttoponconst  23108  cnmptc  23173  cnmptkc  23190  pt1hmeo  23317  tmdgsum2  23607  tsms0  23653  tgptsmscls  23661  resspwsds  23885  imasdsf1olem  23886  nmoeq0  24260  idnghm  24267  rrxcph  24916  ovolctb  25014  ovoliunnul  25031  vitalilem4  25135  vitalilem5  25136  ismbf  25152  mbfconst  25157  mbfss  25170  mbfmulc2re  25172  mbfneg  25174  mbfmulc2  25187  itg11  25215  itg2const  25265  itg2mulclem  25271  itg2mulc  25272  itg2monolem1  25275  itg0  25304  itgz  25305  itgvallem3  25310  iblposlem  25316  i1fibl  25332  itgitg1  25333  itgge0  25335  iblconst  25342  itgconst  25343  itgfsum  25351  iblmulc2  25355  itgmulc2lem1  25356  bddmulibl  25363  bddiblnc  25366  dvcmulf  25469  dvexp  25477  dvexp2  25478  dvmptid  25481  dvmptc  25482  dvef  25504  rolle  25514  dv11cn  25525  ftc1lem4  25563  ftc2  25568  tdeglem4  25584  tdeglem4OLD  25585  ply1nzb  25647  plyconst  25727  plyeq0lem  25731  plypf1  25733  coeeulem  25745  plyco  25762  0dgr  25766  0dgrb  25767  dgrcolem2  25795  dgrco  25796  plyremlem  25824  elqaalem3  25841  iaa  25845  taylply2  25887  itgulm  25927  amgmlem  26501  lgam1  26575  ftalem7  26590  basellem8  26599  dchrfi  26765  dchrptlem3  26776  bra0  31241  padct  31982  cshw1s2  32162  evls1fpws  32691  fedgmullem2  32774  zar0ring  32927  xrge0mulc1cn  32990  esumnul  33115  esum0  33116  esumcvg  33153  ofcc  33173  mbfmcst  33327  sibf0  33402  0rrv  33519  ccatmulgnn0dir  33622  plymul02  33626  plymulx  33628  txsconnlem  34300  cvmliftphtlem  34377  faclim  34785  matunitlindflem1  36570  poimirlem30  36604  ovoliunnfl  36616  voliunnfl  36618  volsupnfl  36619  itg2addnclem  36625  iblmulc2nc  36639  itgmulc2nclem1  36640  itgmulc2nclem2  36641  itgmulc2nc  36642  itgabsnc  36643  ftc1cnnclem  36645  ftc1anclem3  36649  ftc1anclem5  36651  ftc1anclem7  36653  ftc1anclem8  36654  ftc2nc  36656  repwsmet  36788  rrnequiv  36789  evlsvvval  41217  fsuppssindlem2  41246  fsuppssind  41247  mzpconstmpt  41560  mzpcompact2lem  41571  mendlmod  42017  mendassa  42018  mnringmulrcld  43069  expgrowthi  43174  expgrowth  43176  binomcxplemrat  43191  binomcxplemnotnn0  43197  climconstmpt  44453  iblconstmpt  44751  iblempty  44760  itgiccshift  44775  itgperiod  44776  itgsbtaddcnst  44777  stoweidlem21  44816  lindsrng01  47227  eufsn  47586  aacllem  47926  amgmlemALT  47928