Theorem fconstmpt 5687

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4581  {copab 5161   ↦ 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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-sn 4582  df-opab 5162  df-mpt 5181  df-xp 5631

This theorem is referenced by:  fconst  6721  fcoconst  7081  fmptsn  7115  rnmptc  7155  fconstmpo  7477  ofc12  7654  caofinvl  7656  caofidlcan  7662  xpexgALT  7927  cantnf  9606  cnfcom2lem  9614  repsconst  14699  harmonic  15786  geomulcvg  15803  vdwlem8  16920  ramcl  16961  pwsvscafval  17419  setcepi  18016  diag2  18172  pws0g  18702  smndex1igid  18833  0frgp  19712  pwsgsum  19915  rrgsupp  20638  lmhmvsca  21001  uvcresum  21752  psrlinv  21915  psrlidm  21921  psrridm  21922  psrass23l  21926  psrass23  21928  mplcoe1  21996  mplcoe3  21997  mplcoe5  21999  mplmon2  22020  evlslem2  22038  evlslem1  22041  evlsvvval  22052  mhpsclcl  22094  psdmul  22113  psdmvr  22116  coe1z  22209  coe1mul2lem1  22213  coe1tm  22219  coe1sclmul  22228  coe1sclmul2  22230  evls1sca  22271  evl1sca  22282  evls1fpws  22317  grpvrinv  22347  mdetunilem9  22568  pttoponconst  23545  cnmptc  23610  cnmptkc  23627  pt1hmeo  23754  tmdgsum2  24044  tsms0  24090  tgptsmscls  24098  resspwsds  24320  imasdsf1olem  24321  nmoeq0  24684  idnghm  24691  rrxcph  25352  ovolctb  25451  ovoliunnul  25468  vitalilem4  25572  vitalilem5  25573  ismbf  25589  mbfconst  25594  mbfss  25607  mbfmulc2re  25609  mbfneg  25611  mbfmulc2  25624  itg11  25652  itg2const  25701  itg2mulclem  25707  itg2mulc  25708  itg2monolem1  25711  itg0  25741  itgz  25742  itgvallem3  25747  iblposlem  25753  i1fibl  25769  itgitg1  25770  itgge0  25772  iblconst  25779  itgconst  25780  itgfsum  25788  iblmulc2  25792  itgmulc2lem1  25793  bddmulibl  25800  bddiblnc  25803  dvcmulf  25908  dvexp  25917  dvexp2  25918  dvmptid  25921  dvmptc  25922  dvef  25944  rolle  25954  dv11cn  25966  ftc1lem4  26006  ftc2  26011  tdeglem4  26025  ply1nzb  26088  plyconst  26171  plyeq0lem  26175  plypf1  26177  coeeulem  26189  plyco  26206  0dgr  26210  0dgrb  26211  dgrcolem2  26240  dgrco  26241  plyremlem  26272  elqaalem3  26289  iaa  26293  taylply2  26335  taylply2OLD  26336  itgulm  26377  amgmlem  26960  lgam1  27034  ftalem7  27049  basellem8  27058  dchrfi  27226  dchrptlem3  27237  bra0  32008  padct  32778  cshw1s2  33023  gsumind  33407  extvfvcl  33682  mplvrpmmhm  33692  esplyfval3  33711  fedgmullem2  33768  extdgfialglem2  33831  zar0ring  34016  xrge0mulc1cn  34079  esumnul  34186  esum0  34187  esumcvg  34224  ofcc  34244  mbfmcst  34397  sibf0  34472  0rrv  34589  ccatmulgnn0dir  34680  plymul02  34684  plymulx  34686  txsconnlem  35415  cvmliftphtlem  35492  faclim  35921  matunitlindflem1  37788  poimirlem30  37822  ovoliunnfl  37834  voliunnfl  37836  volsupnfl  37837  itg2addnclem  37843  iblmulc2nc  37857  itgmulc2nclem1  37858  itgmulc2nclem2  37859  itgmulc2nc  37860  itgabsnc  37861  ftc1cnnclem  37863  ftc1anclem3  37867  ftc1anclem5  37869  ftc1anclem7  37871  ftc1anclem8  37872  ftc2nc  37874  repwsmet  38006  rrnequiv  38007  fsuppssindlem2  42871  fsuppssind  42872  mzpconstmpt  43018  mzpcompact2lem  43029  mendlmod  43467  mendassa  43468  mnringmulrcld  44505  expgrowthi  44610  expgrowth  44612  binomcxplemrat  44627  binomcxplemnotnn0  44633  climconstmpt  45938  iblconstmpt  46236  iblempty  46245  itgiccshift  46260  itgperiod  46261  itgsbtaddcnst  46262  stoweidlem21  46301  nthrucw  47166  cjnpoly  47171  lindsrng01  48750  eufsn  49123  diag1a  49586  aacllem  50082  amgmlemALT  50084