Theorem fconstmpt 5721

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 4603	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 635	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5176	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5665	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5191	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2795	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {csn 4587  {copab 5171   ↦ cmpt 5190   × cxp 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-sn 4588  df-opab 5172  df-mpt 5191  df-xp 5665

This theorem is used by:  fconst  6765  fcoconst  7131  fmptsn  7168  rnmptc  7209  fconstmpo  7533  ofc12  7711  caofinvl  7713  caofidlcan  7719  xpexgALT  7981  cantnf  9675  cnfcom2lem  9683  repsconst  14845  harmonic  15950  geomulcvg  15967  vdwlem8  17084  ramcl  17125  pwsvscafval  17584  setcepi  18181  diag2  18337  pws0g  18882  smndex1gbas  19012  smndex1gid  19014  smndex1igid  19016  smndex1igidOLD  19017  0frgp  19907  pwsgsum  20110  rrgsupp  20864  lmhmvsca  21230  uvcresum  22007  psrlinv  22171  psrlidm  22177  psrridm  22178  psrass23l  22182  psrass23  22184  mplcoe1  22254  mplcoe3  22255  mplcoe5  22257  mplmon2  22278  evlslem2  22296  evlslem1  22299  evlsvvval  22310  mhpsclcl  22376  psdmul  22395  psdmvr  22398  coe1z  22490  coe1mul2lem1  22494  coe1tm  22500  coe1sclmul  22509  coe1sclmul2  22511  evls1sca  22549  evl1sca  22560  evls1fpws  22595  grpvrinv  22622  mdetunilem9  22843  matunitlindflem1  22902  pttoponconst  23824  cnmptc  23889  cnmptkc  23906  pt1hmeo  24033  tmdgsum2  24323  tsms0  24369  tgptsmscls  24377  resspwsds  24599  imasdsf1olem  24600  nmoeq0  24963  idnghm  24970  rrxcph  25621  ovolctb  25719  ovoliunnul  25736  vitalilem4  25840  vitalilem5  25841  ismbf  25857  mbfconst  25862  mbfss  25875  mbfmulc2re  25877  mbfneg  25879  mbfmulc2  25892  itg11  25920  itg2const  25969  itg2mulclem  25975  itg2mulc  25976  itg2monolem1  25979  itg0  26009  itgz  26010  itgvallem3  26015  iblposlem  26021  i1fibl  26037  itgitg1  26038  itgge0  26040  iblconst  26047  itgconst  26048  itgfsum  26056  iblmulc2  26060  itgmulc2lem1  26061  bddmulibl  26068  bddiblnc  26071  dvcmulf  26174  dvexp  26182  dvexp2  26183  dvmptid  26186  dvmptc  26187  dvef  26209  rolle  26219  dv11cn  26230  ftc1lem4  26268  ftc2  26273  tdeglem4  26287  ply1nzb  26350  plyconst  26433  plyeq0lem  26437  plypf1  26439  coeeulem  26451  plyco  26468  0dgr  26472  0dgrb  26473  dgrcolem2  26501  dgrco  26502  plymul02  26511  plymulidp  26513  plyremlem  26535  elqaalem3  26552  iaa  26558  taylply2  26601  itgulm  26641  amgmlem  27224  lgam1  27298  ftalem7  27313  basellem8  27322  dchrfi  27489  dchrptlem3  27500  istrkg2ld  28799  bra0  32417  padct  33176  cshw1s2  33387  gsumind  33772  mplasclco  34013  selvply1rhmlem2  34018  selvply1rhm0  34023  extvfvcl  34033  mplvrpmmhm  34043  psrgsum  34045  psrmonprod  34049  esplyfval3  34069  fedgmullem2  34127  extdgfialglem2  34190  zar0ring  34375  xrge0mulc1cn  34438  esumnul  34545  esum0  34546  esumcvg  34583  ofcc  34603  mbfmcst  34757  sibf0  34832  0rrv  34949  ccatmulgnn0dir  35040  txsconnlem  35806  cvmliftphtlem  35883  faclim  36312  poimirlem30  38386  ovoliunnfl  38398  voliunnfl  38400  volsupnfl  38401  itg2addnclem  38407  iblmulc2nc  38421  itgmulc2nclem1  38422  itgmulc2nclem2  38423  itgmulc2nc  38424  itgabsnc  38425  ftc1cnnclem  38427  ftc1anclem3  38431  ftc1anclem5  38433  ftc1anclem7  38435  ftc1anclem8  38436  ftc2nc  38438  repwsmet  38571  rrnequiv  38572  fsuppssindlem2  43425  fsuppssind  43426  mzpconstmpt  43572  mzpcompact2lem  43583  mendlmod  44017  mendassa  44018  mnringmulrcld  45053  expgrowthi  45144  expgrowth  45146  binomcxplemrat  45161  binomcxplemnotnn0  45167  climconstmpt  46473  iblconstmpt  46771  iblempty  46780  itgiccshift  46795  itgperiod  46796  itgsbtaddcnst  46797  stoweidlem21  46836  hoicvr  47363  cjnpoly  47744  lindsrng01  49385  eufsn  49757  diag1a  50218  aacllem  50759  veroquadmodzerod  50804  amgmlemALT  50808