Theorem fconstmpt 5685

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

Syntax hints:   ∧ wa 397   = wceq 1541   ∈ wcel 2106  {csn 4578  {copab 5159   ↦ cmpt 5180   × cxp 5623

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 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3444  df-sn 4579  df-opab 5160  df-mpt 5181  df-xp 5631

This theorem is referenced by:  fconst  6716  fcoconst  7067  fmptsn  7100  rnmptc  7143  rnmptcOLD  7144  fconstmpo  7458  ofc12  7628  caofinvl  7630  xpexgALT  7897  cantnf  9555  cnfcom2lem  9563  repsconst  14584  harmonic  15671  geomulcvg  15688  vdwlem8  16787  ramcl  16828  pwsvscafval  17303  setcepi  17901  diag2  18061  pws0g  18519  smndex1igid  18640  0frgp  19481  pwsgsum  19678  lmhmvsca  20413  rrgsupp  20668  uvcresum  21106  psrlinv  21272  psrlidm  21278  psrridm  21279  psrass23l  21283  psrass23  21285  mplcoe1  21344  mplcoe3  21345  mplcoe5  21347  mplmon2  21375  evlslem2  21395  evlslem1  21398  mhpsclcl  21443  coe1z  21540  coe1mul2lem1  21544  coe1tm  21550  coe1sclmul  21559  coe1sclmul2  21561  evls1sca  21595  evl1sca  21606  grpvrinv  21651  mdetunilem9  21875  pttoponconst  22854  cnmptc  22919  cnmptkc  22936  pt1hmeo  23063  tmdgsum2  23353  tsms0  23399  tgptsmscls  23407  resspwsds  23631  imasdsf1olem  23632  nmoeq0  24006  idnghm  24013  rrxcph  24662  ovolctb  24760  ovoliunnul  24777  vitalilem4  24881  vitalilem5  24882  ismbf  24898  mbfconst  24903  mbfss  24916  mbfmulc2re  24918  mbfneg  24920  mbfmulc2  24933  itg11  24961  itg2const  25011  itg2mulclem  25017  itg2mulc  25018  itg2monolem1  25021  itg0  25050  itgz  25051  itgvallem3  25056  iblposlem  25062  i1fibl  25078  itgitg1  25079  itgge0  25081  iblconst  25088  itgconst  25089  itgfsum  25097  iblmulc2  25101  itgmulc2lem1  25102  bddmulibl  25109  bddiblnc  25112  dvcmulf  25215  dvexp  25223  dvexp2  25224  dvmptid  25227  dvmptc  25228  dvef  25250  rolle  25260  dv11cn  25271  ftc1lem4  25309  ftc2  25314  tdeglem4  25330  tdeglem4OLD  25331  ply1nzb  25393  plyconst  25473  plyeq0lem  25477  plypf1  25479  coeeulem  25491  plyco  25508  0dgr  25512  0dgrb  25513  dgrcolem2  25541  dgrco  25542  plyremlem  25570  elqaalem3  25587  iaa  25591  taylply2  25633  itgulm  25673  amgmlem  26245  lgam1  26319  ftalem7  26334  basellem8  26343  dchrfi  26509  dchrptlem3  26520  bra0  30600  padct  31339  cshw1s2  31517  fedgmullem2  32007  zar0ring  32124  xrge0mulc1cn  32187  esumnul  32312  esum0  32313  esumcvg  32350  ofcc  32370  mbfmcst  32524  sibf0  32599  0rrv  32716  ccatmulgnn0dir  32819  plymul02  32823  plymulx  32825  txsconnlem  33499  cvmliftphtlem  33576  faclim  34002  matunitlindflem1  35927  poimirlem30  35961  ovoliunnfl  35973  voliunnfl  35975  volsupnfl  35976  itg2addnclem  35982  iblmulc2nc  35996  itgmulc2nclem1  35997  itgmulc2nclem2  35998  itgmulc2nc  35999  itgabsnc  36000  ftc1cnnclem  36002  ftc1anclem3  36006  ftc1anclem5  36008  ftc1anclem7  36010  ftc1anclem8  36011  ftc2nc  36013  repwsmet  36146  rrnequiv  36147  evlsbagval  40584  fsuppssindlem2  40590  fsuppssind  40591  mzpconstmpt  40873  mzpcompact2lem  40884  mendlmod  41330  mendassa  41331  mnringmulrcld  42217  expgrowthi  42322  expgrowth  42324  binomcxplemrat  42339  binomcxplemnotnn0  42345  climconstmpt  43585  iblconstmpt  43883  iblempty  43892  itgiccshift  43907  itgperiod  43908  itgsbtaddcnst  43909  stoweidlem21  43948  lindsrng01  46225  eufsn  46585  aacllem  46921  amgmlemALT  46923