Theorem fconstmpt 5650

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

Syntax hints:   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {csn 4562  {copab 5137   ↦ cmpt 5158   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-sn 4563  df-opab 5138  df-mpt 5159  df-xp 5596

This theorem is referenced by:  fconst  6669  fcoconst  7015  fmptsn  7048  rnmptc  7091  rnmptcOLD  7092  fconstmpo  7400  ofc12  7570  caofinvl  7572  xpexgALT  7833  cantnf  9460  cnfcom2lem  9468  repsconst  14494  harmonic  15580  geomulcvg  15597  vdwlem8  16698  ramcl  16739  pwsvscafval  17214  setcepi  17812  diag2  17972  pws0g  18430  smndex1igid  18552  0frgp  19394  pwsgsum  19592  lmhmvsca  20316  rrgsupp  20571  uvcresum  21009  psrlinv  21175  psrlidm  21181  psrridm  21182  psrass23l  21186  psrass23  21188  mplcoe1  21247  mplcoe3  21248  mplcoe5  21250  mplmon2  21278  evlslem2  21298  evlslem1  21301  mhpsclcl  21346  coe1z  21443  coe1mul2lem1  21447  coe1tm  21453  coe1sclmul  21462  coe1sclmul2  21464  evls1sca  21498  evl1sca  21509  grpvrinv  21554  mdetunilem9  21778  pttoponconst  22757  cnmptc  22822  cnmptkc  22839  pt1hmeo  22966  tmdgsum2  23256  tsms0  23302  tgptsmscls  23310  resspwsds  23534  imasdsf1olem  23535  nmoeq0  23909  idnghm  23916  rrxcph  24565  ovolctb  24663  ovoliunnul  24680  vitalilem4  24784  vitalilem5  24785  ismbf  24801  mbfconst  24806  mbfss  24819  mbfmulc2re  24821  mbfneg  24823  mbfmulc2  24836  itg11  24864  itg2const  24914  itg2mulclem  24920  itg2mulc  24921  itg2monolem1  24924  itg0  24953  itgz  24954  itgvallem3  24959  iblposlem  24965  i1fibl  24981  itgitg1  24982  itgge0  24984  iblconst  24991  itgconst  24992  itgfsum  25000  iblmulc2  25004  itgmulc2lem1  25005  bddmulibl  25012  bddiblnc  25015  dvcmulf  25118  dvexp  25126  dvexp2  25127  dvmptid  25130  dvmptc  25131  dvef  25153  rolle  25163  dv11cn  25174  ftc1lem4  25212  ftc2  25217  tdeglem4  25233  tdeglem4OLD  25234  ply1nzb  25296  plyconst  25376  plyeq0lem  25380  plypf1  25382  coeeulem  25394  plyco  25411  0dgr  25415  0dgrb  25416  dgrcolem2  25444  dgrco  25445  plyremlem  25473  elqaalem3  25490  iaa  25494  taylply2  25536  itgulm  25576  amgmlem  26148  lgam1  26222  ftalem7  26237  basellem8  26246  dchrfi  26412  dchrptlem3  26423  bra0  30321  padct  31063  cshw1s2  31241  fedgmullem2  31720  zar0ring  31837  xrge0mulc1cn  31900  esumnul  32025  esum0  32026  esumcvg  32063  ofcc  32083  mbfmcst  32235  sibf0  32310  0rrv  32427  ccatmulgnn0dir  32530  plymul02  32534  plymulx  32536  txsconnlem  33211  cvmliftphtlem  33288  faclim  33721  matunitlindflem1  35782  poimirlem30  35816  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  itg2addnclem  35837  iblmulc2nc  35851  itgmulc2nclem1  35852  itgmulc2nclem2  35853  itgmulc2nc  35854  itgabsnc  35855  ftc1cnnclem  35857  ftc1anclem3  35861  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anclem8  35866  ftc2nc  35868  repwsmet  36001  rrnequiv  36002  evlsbagval  40282  fsuppssindlem2  40288  fsuppssind  40289  mzpconstmpt  40569  mzpcompact2lem  40580  mendlmod  41025  mendassa  41026  mnringmulrcld  41853  expgrowthi  41958  expgrowth  41960  binomcxplemrat  41975  binomcxplemnotnn0  41981  climconstmpt  43206  iblconstmpt  43504  iblempty  43513  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  stoweidlem21  43569  lindsrng01  45820  eufsn  46180  aacllem  46516  amgmlemALT  46518