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  7082  fmptsn  7116  rnmptc  7156  fconstmpo  7478  ofc12  7655  caofinvl  7657  caofidlcan  7663  xpexgALT  7928  cantnf  9607  cnfcom2lem  9615  repsconst  14700  harmonic  15787  geomulcvg  15804  vdwlem8  16921  ramcl  16962  pwsvscafval  17420  setcepi  18017  diag2  18173  pws0g  18703  smndex1igid  18834  0frgp  19713  pwsgsum  19916  rrgsupp  20639  lmhmvsca  21002  uvcresum  21753  psrlinv  21916  psrlidm  21922  psrridm  21923  psrass23l  21927  psrass23  21929  mplcoe1  21997  mplcoe3  21998  mplcoe5  22000  mplmon2  22021  evlslem2  22039  evlslem1  22042  evlsvvval  22053  mhpsclcl  22095  psdmul  22114  psdmvr  22117  coe1z  22210  coe1mul2lem1  22214  coe1tm  22220  coe1sclmul  22229  coe1sclmul2  22231  evls1sca  22272  evl1sca  22283  evls1fpws  22318  grpvrinv  22348  mdetunilem9  22569  pttoponconst  23546  cnmptc  23611  cnmptkc  23628  pt1hmeo  23755  tmdgsum2  24045  tsms0  24091  tgptsmscls  24099  resspwsds  24321  imasdsf1olem  24322  nmoeq0  24685  idnghm  24692  rrxcph  25353  ovolctb  25452  ovoliunnul  25469  vitalilem4  25573  vitalilem5  25574  ismbf  25590  mbfconst  25595  mbfss  25608  mbfmulc2re  25610  mbfneg  25612  mbfmulc2  25625  itg11  25653  itg2const  25702  itg2mulclem  25708  itg2mulc  25709  itg2monolem1  25712  itg0  25742  itgz  25743  itgvallem3  25748  iblposlem  25754  i1fibl  25770  itgitg1  25771  itgge0  25773  iblconst  25780  itgconst  25781  itgfsum  25789  iblmulc2  25793  itgmulc2lem1  25794  bddmulibl  25801  bddiblnc  25804  dvcmulf  25909  dvexp  25918  dvexp2  25919  dvmptid  25922  dvmptc  25923  dvef  25945  rolle  25955  dv11cn  25967  ftc1lem4  26007  ftc2  26012  tdeglem4  26026  ply1nzb  26089  plyconst  26172  plyeq0lem  26176  plypf1  26178  coeeulem  26190  plyco  26207  0dgr  26211  0dgrb  26212  dgrcolem2  26241  dgrco  26242  plyremlem  26273  elqaalem3  26290  iaa  26294  taylply2  26336  taylply2OLD  26337  itgulm  26378  amgmlem  26961  lgam1  27035  ftalem7  27050  basellem8  27059  dchrfi  27227  dchrptlem3  27238  bra0  32030  padct  32800  cshw1s2  33045  gsumind  33430  extvfvcl  33705  mplvrpmmhm  33715  psrgsum  33717  psrmonprod  33721  esplyfval3  33741  fedgmullem2  33800  extdgfialglem2  33863  zar0ring  34048  xrge0mulc1cn  34111  esumnul  34218  esum0  34219  esumcvg  34256  ofcc  34276  mbfmcst  34429  sibf0  34504  0rrv  34621  ccatmulgnn0dir  34712  plymul02  34716  plymulx  34718  txsconnlem  35447  cvmliftphtlem  35524  faclim  35953  matunitlindflem1  37830  poimirlem30  37864  ovoliunnfl  37876  voliunnfl  37878  volsupnfl  37879  itg2addnclem  37885  iblmulc2nc  37899  itgmulc2nclem1  37900  itgmulc2nclem2  37901  itgmulc2nc  37902  itgabsnc  37903  ftc1cnnclem  37905  ftc1anclem3  37909  ftc1anclem5  37911  ftc1anclem7  37913  ftc1anclem8  37914  ftc2nc  37916  repwsmet  38048  rrnequiv  38049  fsuppssindlem2  42913  fsuppssind  42914  mzpconstmpt  43060  mzpcompact2lem  43071  mendlmod  43509  mendassa  43510  mnringmulrcld  44547  expgrowthi  44652  expgrowth  44654  binomcxplemrat  44669  binomcxplemnotnn0  44675  climconstmpt  45979  iblconstmpt  46277  iblempty  46286  itgiccshift  46301  itgperiod  46302  itgsbtaddcnst  46303  stoweidlem21  46342  nthrucw  47207  cjnpoly  47212  lindsrng01  48791  eufsn  49164  diag1a  49627  aacllem  50123  amgmlemALT  50125