Theorem fconstmpt 5716

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {csn 4601  {copab 5181   ↦ cmpt 5201   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-sn 4602  df-opab 5182  df-mpt 5202  df-xp 5660

This theorem is referenced by:  fconst  6763  fcoconst  7123  fmptsn  7158  rnmptc  7198  fconstmpo  7522  ofc12  7699  caofinvl  7701  caofidlcan  7707  xpexgALT  7978  cantnf  9705  cnfcom2lem  9713  repsconst  14788  harmonic  15873  geomulcvg  15890  vdwlem8  17006  ramcl  17047  pwsvscafval  17506  setcepi  18099  diag2  18255  pws0g  18749  smndex1igid  18880  0frgp  19758  pwsgsum  19961  rrgsupp  20659  lmhmvsca  21001  uvcresum  21751  psrlinv  21913  psrlidm  21920  psrridm  21921  psrass23l  21925  psrass23  21927  mplcoe1  21993  mplcoe3  21994  mplcoe5  21996  mplmon2  22017  evlslem2  22035  evlslem1  22038  mhpsclcl  22083  psdmul  22102  psdmvr  22105  coe1z  22198  coe1mul2lem1  22202  coe1tm  22208  coe1sclmul  22217  coe1sclmul2  22219  evls1sca  22259  evl1sca  22270  evls1fpws  22305  grpvrinv  22335  mdetunilem9  22556  pttoponconst  23533  cnmptc  23598  cnmptkc  23615  pt1hmeo  23742  tmdgsum2  24032  tsms0  24078  tgptsmscls  24086  resspwsds  24309  imasdsf1olem  24310  nmoeq0  24673  idnghm  24680  rrxcph  25342  ovolctb  25441  ovoliunnul  25458  vitalilem4  25562  vitalilem5  25563  ismbf  25579  mbfconst  25584  mbfss  25597  mbfmulc2re  25599  mbfneg  25601  mbfmulc2  25614  itg11  25642  itg2const  25691  itg2mulclem  25697  itg2mulc  25698  itg2monolem1  25701  itg0  25731  itgz  25732  itgvallem3  25737  iblposlem  25743  i1fibl  25759  itgitg1  25760  itgge0  25762  iblconst  25769  itgconst  25770  itgfsum  25778  iblmulc2  25782  itgmulc2lem1  25783  bddmulibl  25790  bddiblnc  25793  dvcmulf  25898  dvexp  25907  dvexp2  25908  dvmptid  25911  dvmptc  25912  dvef  25934  rolle  25944  dv11cn  25956  ftc1lem4  25996  ftc2  26001  tdeglem4  26015  ply1nzb  26078  plyconst  26161  plyeq0lem  26165  plypf1  26167  coeeulem  26179  plyco  26196  0dgr  26200  0dgrb  26201  dgrcolem2  26230  dgrco  26231  plyremlem  26262  elqaalem3  26279  iaa  26283  taylply2  26325  taylply2OLD  26326  itgulm  26367  amgmlem  26950  lgam1  27024  ftalem7  27039  basellem8  27048  dchrfi  27216  dchrptlem3  27227  bra0  31877  padct  32643  cshw1s2  32882  fedgmullem2  33616  zar0ring  33855  xrge0mulc1cn  33918  esumnul  34025  esum0  34026  esumcvg  34063  ofcc  34083  mbfmcst  34237  sibf0  34312  0rrv  34429  ccatmulgnn0dir  34520  plymul02  34524  plymulx  34526  txsconnlem  35208  cvmliftphtlem  35285  faclim  35709  matunitlindflem1  37586  poimirlem30  37620  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  itg2addnclem  37641  iblmulc2nc  37655  itgmulc2nclem1  37656  itgmulc2nclem2  37657  itgmulc2nc  37658  itgabsnc  37659  ftc1cnnclem  37661  ftc1anclem3  37665  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  ftc2nc  37672  repwsmet  37804  rrnequiv  37805  evlsvvval  42533  fsuppssindlem2  42562  fsuppssind  42563  mzpconstmpt  42710  mzpcompact2lem  42721  mendlmod  43160  mendassa  43161  mnringmulrcld  44200  expgrowthi  44305  expgrowth  44307  binomcxplemrat  44322  binomcxplemnotnn0  44328  climconstmpt  45635  iblconstmpt  45933  iblempty  45942  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  stoweidlem21  45998  lindsrng01  48392  eufsn  48768  diag1a  49164  aacllem  49613  amgmlemALT  49615