Theorem fconstmpt 5682

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4557  {copab 5136   ↦ cmpt 5155   × cxp 5618

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-sn 4558  df-opab 5137  df-mpt 5156  df-xp 5626

This theorem is referenced by:  fconst  6715  fcoconst  7076  fmptsn  7111  rnmptc  7151  fconstmpo  7473  ofc12  7650  caofinvl  7652  caofidlcan  7658  xpexgALT  7923  cantnf  9603  cnfcom2lem  9611  repsconst  14723  harmonic  15813  geomulcvg  15830  vdwlem8  16948  ramcl  16989  pwsvscafval  17447  setcepi  18044  diag2  18200  pws0g  18730  smndex1gbas  18859  smndex1gid  18861  smndex1igid  18863  smndex1igidOLD  18864  0frgp  19743  pwsgsum  19946  rrgsupp  20667  lmhmvsca  21029  uvcresum  21762  psrlinv  21923  psrlidm  21929  psrridm  21930  psrass23l  21934  psrass23  21936  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  mplmon2  22028  evlslem2  22046  evlslem1  22049  evlsvvval  22060  mhpsclcl  22102  psdmul  22121  psdmvr  22124  coe1z  22216  coe1mul2lem1  22220  coe1tm  22226  coe1sclmul  22235  coe1sclmul2  22237  evls1sca  22276  evl1sca  22287  evls1fpws  22322  grpvrinv  22352  mdetunilem9  22573  pttoponconst  23550  cnmptc  23615  cnmptkc  23632  pt1hmeo  23759  tmdgsum2  24049  tsms0  24095  tgptsmscls  24103  resspwsds  24325  imasdsf1olem  24326  nmoeq0  24689  idnghm  24696  rrxcph  25347  ovolctb  25445  ovoliunnul  25462  vitalilem4  25566  vitalilem5  25567  ismbf  25583  mbfconst  25588  mbfss  25601  mbfmulc2re  25603  mbfneg  25605  mbfmulc2  25618  itg11  25646  itg2const  25695  itg2mulclem  25701  itg2mulc  25702  itg2monolem1  25705  itg0  25735  itgz  25736  itgvallem3  25741  iblposlem  25747  i1fibl  25763  itgitg1  25764  itgge0  25766  iblconst  25773  itgconst  25774  itgfsum  25782  iblmulc2  25786  itgmulc2lem1  25787  bddmulibl  25794  bddiblnc  25797  dvcmulf  25900  dvexp  25908  dvexp2  25909  dvmptid  25912  dvmptc  25913  dvef  25935  rolle  25945  dv11cn  25956  ftc1lem4  25994  ftc2  25999  tdeglem4  26013  ply1nzb  26076  plyconst  26159  plyeq0lem  26163  plypf1  26165  coeeulem  26177  plyco  26194  0dgr  26198  0dgrb  26199  dgrcolem2  26227  dgrco  26228  plyremlem  26258  elqaalem3  26275  iaa  26279  taylply2  26321  itgulm  26361  amgmlem  26941  lgam1  27015  ftalem7  27030  basellem8  27039  dchrfi  27206  dchrptlem3  27217  istrkg2ld  28516  bra0  32009  padct  32779  cshw1s2  33008  gsumind  33393  extvfvcl  33668  mplvrpmmhm  33678  psrgsum  33680  psrmonprod  33684  esplyfval3  33704  fedgmullem2  33762  extdgfialglem2  33825  zar0ring  34010  xrge0mulc1cn  34073  esumnul  34180  esum0  34181  esumcvg  34218  ofcc  34238  mbfmcst  34391  sibf0  34466  0rrv  34583  ccatmulgnn0dir  34674  plymul02  34678  plymulx  34680  txsconnlem  35410  cvmliftphtlem  35487  faclim  35916  matunitlindflem1  37925  poimirlem30  37959  ovoliunnfl  37971  voliunnfl  37973  volsupnfl  37974  itg2addnclem  37980  iblmulc2nc  37994  itgmulc2nclem1  37995  itgmulc2nclem2  37996  itgmulc2nc  37997  itgabsnc  37998  ftc1cnnclem  38000  ftc1anclem3  38004  ftc1anclem5  38006  ftc1anclem7  38008  ftc1anclem8  38009  ftc2nc  38011  repwsmet  38143  rrnequiv  38144  fsuppssindlem2  43013  fsuppssind  43014  mzpconstmpt  43160  mzpcompact2lem  43171  mendlmod  43605  mendassa  43606  mnringmulrcld  44643  expgrowthi  44748  expgrowth  44750  binomcxplemrat  44765  binomcxplemnotnn0  44771  climconstmpt  46074  iblconstmpt  46372  iblempty  46381  itgiccshift  46396  itgperiod  46397  itgsbtaddcnst  46398  stoweidlem21  46437  hoicvr  46964  nthrucw  47304  cjnpoly  47325  lindsrng01  48932  eufsn  49305  diag1a  49768  aacllem  50264  amgmlemALT  50266