Theorem fconstmpt 5734

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 4640	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 622	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5209	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5678	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5226	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2765	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1534   ∈ wcel 2099  {csn 4624  {copab 5204   ↦ cmpt 5225   × cxp 5670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-sn 4625  df-opab 5205  df-mpt 5226  df-xp 5678

This theorem is referenced by:  fconst  6777  fcoconst  7137  fmptsn  7170  rnmptc  7213  fconstmpo  7531  ofc12  7707  caofinvl  7709  xpexgALT  7979  cantnf  9708  cnfcom2lem  9716  repsconst  14746  harmonic  15829  geomulcvg  15846  vdwlem8  16948  ramcl  16989  pwsvscafval  17467  setcepi  18068  diag2  18228  pws0g  18721  smndex1igid  18847  0frgp  19725  pwsgsum  19928  lmhmvsca  20919  rrgsupp  21227  uvcresum  21714  psrlinv  21885  psrlidm  21892  psrridm  21893  psrass23l  21897  psrass23  21899  mplcoe1  21962  mplcoe3  21963  mplcoe5  21965  mplmon2  21992  evlslem2  22012  evlslem1  22015  mhpsclcl  22058  psdmul  22077  coe1z  22169  coe1mul2lem1  22173  coe1tm  22179  coe1sclmul  22188  coe1sclmul2  22190  evls1sca  22229  evl1sca  22240  grpvrinv  22285  mdetunilem9  22509  pttoponconst  23488  cnmptc  23553  cnmptkc  23570  pt1hmeo  23697  tmdgsum2  23987  tsms0  24033  tgptsmscls  24041  resspwsds  24265  imasdsf1olem  24266  nmoeq0  24640  idnghm  24647  rrxcph  25307  ovolctb  25406  ovoliunnul  25423  vitalilem4  25527  vitalilem5  25528  ismbf  25544  mbfconst  25549  mbfss  25562  mbfmulc2re  25564  mbfneg  25566  mbfmulc2  25579  itg11  25607  itg2const  25657  itg2mulclem  25663  itg2mulc  25664  itg2monolem1  25667  itg0  25696  itgz  25697  itgvallem3  25702  iblposlem  25708  i1fibl  25724  itgitg1  25725  itgge0  25727  iblconst  25734  itgconst  25735  itgfsum  25743  iblmulc2  25747  itgmulc2lem1  25748  bddmulibl  25755  bddiblnc  25758  dvcmulf  25863  dvexp  25872  dvexp2  25873  dvmptid  25876  dvmptc  25877  dvef  25899  rolle  25909  dv11cn  25921  ftc1lem4  25961  ftc2  25966  tdeglem4  25982  tdeglem4OLD  25983  ply1nzb  26045  plyconst  26127  plyeq0lem  26131  plypf1  26133  coeeulem  26145  plyco  26162  0dgr  26166  0dgrb  26167  dgrcolem2  26196  dgrco  26197  plyremlem  26226  elqaalem3  26243  iaa  26247  taylply2  26289  taylply2OLD  26290  itgulm  26331  amgmlem  26909  lgam1  26983  ftalem7  26998  basellem8  27007  dchrfi  27175  dchrptlem3  27186  bra0  31747  padct  32485  cshw1s2  32663  evls1fpws  33182  fedgmullem2  33260  zar0ring  33415  xrge0mulc1cn  33478  esumnul  33603  esum0  33604  esumcvg  33641  ofcc  33661  mbfmcst  33815  sibf0  33890  0rrv  34007  ccatmulgnn0dir  34110  plymul02  34114  plymulx  34116  txsconnlem  34786  cvmliftphtlem  34863  faclim  35276  matunitlindflem1  37024  poimirlem30  37058  ovoliunnfl  37070  voliunnfl  37072  volsupnfl  37073  itg2addnclem  37079  iblmulc2nc  37093  itgmulc2nclem1  37094  itgmulc2nclem2  37095  itgmulc2nc  37096  itgabsnc  37097  ftc1cnnclem  37099  ftc1anclem3  37103  ftc1anclem5  37105  ftc1anclem7  37107  ftc1anclem8  37108  ftc2nc  37110  repwsmet  37242  rrnequiv  37243  evlsvvval  41718  fsuppssindlem2  41747  fsuppssind  41748  mzpconstmpt  42082  mzpcompact2lem  42093  mendlmod  42539  mendassa  42540  mnringmulrcld  43588  expgrowthi  43693  expgrowth  43695  binomcxplemrat  43710  binomcxplemnotnn0  43716  climconstmpt  44969  iblconstmpt  45267  iblempty  45276  itgiccshift  45291  itgperiod  45292  itgsbtaddcnst  45293  stoweidlem21  45332  lindsrng01  47459  eufsn  47817  aacllem  48157  amgmlemALT  48159