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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4579  {copab 5157   ↦ cmpt 5176   × cxp 5621

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-sn 4580  df-opab 5158  df-mpt 5177  df-xp 5629

This theorem is referenced by:  fconst  6714  fcoconst  7072  fmptsn  7107  rnmptc  7147  fconstmpo  7470  ofc12  7647  caofinvl  7649  caofidlcan  7655  xpexgALT  7923  cantnf  9608  cnfcom2lem  9616  repsconst  14696  harmonic  15784  geomulcvg  15801  vdwlem8  16918  ramcl  16959  pwsvscafval  17416  setcepi  18013  diag2  18169  pws0g  18665  smndex1igid  18796  0frgp  19676  pwsgsum  19879  rrgsupp  20604  lmhmvsca  20967  uvcresum  21718  psrlinv  21880  psrlidm  21887  psrridm  21888  psrass23l  21892  psrass23  21894  mplcoe1  21960  mplcoe3  21961  mplcoe5  21963  mplmon2  21984  evlslem2  22002  evlslem1  22005  mhpsclcl  22050  psdmul  22069  psdmvr  22072  coe1z  22165  coe1mul2lem1  22169  coe1tm  22175  coe1sclmul  22184  coe1sclmul2  22186  evls1sca  22226  evl1sca  22237  evls1fpws  22272  grpvrinv  22302  mdetunilem9  22523  pttoponconst  23500  cnmptc  23565  cnmptkc  23582  pt1hmeo  23709  tmdgsum2  23999  tsms0  24045  tgptsmscls  24053  resspwsds  24276  imasdsf1olem  24277  nmoeq0  24640  idnghm  24647  rrxcph  25308  ovolctb  25407  ovoliunnul  25424  vitalilem4  25528  vitalilem5  25529  ismbf  25545  mbfconst  25550  mbfss  25563  mbfmulc2re  25565  mbfneg  25567  mbfmulc2  25580  itg11  25608  itg2const  25657  itg2mulclem  25663  itg2mulc  25664  itg2monolem1  25667  itg0  25697  itgz  25698  itgvallem3  25703  iblposlem  25709  i1fibl  25725  itgitg1  25726  itgge0  25728  iblconst  25735  itgconst  25736  itgfsum  25744  iblmulc2  25748  itgmulc2lem1  25749  bddmulibl  25756  bddiblnc  25759  dvcmulf  25864  dvexp  25873  dvexp2  25874  dvmptid  25877  dvmptc  25878  dvef  25900  rolle  25910  dv11cn  25922  ftc1lem4  25962  ftc2  25967  tdeglem4  25981  ply1nzb  26044  plyconst  26127  plyeq0lem  26131  plypf1  26133  coeeulem  26145  plyco  26162  0dgr  26166  0dgrb  26167  dgrcolem2  26196  dgrco  26197  plyremlem  26228  elqaalem3  26245  iaa  26249  taylply2  26291  taylply2OLD  26292  itgulm  26333  amgmlem  26916  lgam1  26990  ftalem7  27005  basellem8  27014  dchrfi  27182  dchrptlem3  27193  bra0  31912  padct  32676  cshw1s2  32915  fedgmullem2  33602  zar0ring  33844  xrge0mulc1cn  33907  esumnul  34014  esum0  34015  esumcvg  34052  ofcc  34072  mbfmcst  34226  sibf0  34301  0rrv  34418  ccatmulgnn0dir  34509  plymul02  34513  plymulx  34515  txsconnlem  35212  cvmliftphtlem  35289  faclim  35718  matunitlindflem1  37595  poimirlem30  37629  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  itg2addnclem  37650  iblmulc2nc  37664  itgmulc2nclem1  37665  itgmulc2nclem2  37666  itgmulc2nc  37667  itgabsnc  37668  ftc1cnnclem  37670  ftc1anclem3  37674  ftc1anclem5  37676  ftc1anclem7  37678  ftc1anclem8  37679  ftc2nc  37681  repwsmet  37813  rrnequiv  37814  evlsvvval  42536  fsuppssindlem2  42565  fsuppssind  42566  mzpconstmpt  42713  mzpcompact2lem  42724  mendlmod  43162  mendassa  43163  mnringmulrcld  44201  expgrowthi  44306  expgrowth  44308  binomcxplemrat  44323  binomcxplemnotnn0  44329  climconstmpt  45640  iblconstmpt  45938  iblempty  45947  itgiccshift  45962  itgperiod  45963  itgsbtaddcnst  45964  stoweidlem21  46003  cjnpoly  46874  lindsrng01  48441  eufsn  48814  diag1a  49278  aacllem  49774  amgmlemALT  49776