Theorem fconstmpt 5710

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 4599	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 632	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5168	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5654	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5183	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2796	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 399   = wceq 1561   ∈ wcel 2143  {csn 4583  {copab 5163   ↦ cmpt 5182   × cxp 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-sn 4584  df-opab 5164  df-mpt 5183  df-xp 5654

This theorem is referenced by:  fconst  6750  fcoconst  7116  fmptsn  7151  rnmptc  7191  fconstmpo  7513  ofc12  7690  caofinvl  7692  caofidlcan  7698  xpexgALT  7962  cantnf  9646  cnfcom2lem  9654  repsconst  14795  harmonic  15899  geomulcvg  15916  vdwlem8  17034  ramcl  17075  pwsvscafval  17534  setcepi  18131  diag2  18287  pws0g  18817  smndex1gbas  18946  smndex1gid  18948  smndex1igid  18950  smndex1igidOLD  18951  0frgp  19829  pwsgsum  20032  rrgsupp  20761  lmhmvsca  21119  uvcresum  21852  psrlinv  22014  psrlidm  22020  psrridm  22021  psrass23l  22025  psrass23  22027  mplcoe1  22097  mplcoe3  22098  mplcoe5  22100  mplmon2  22121  evlslem2  22139  evlslem1  22142  evlsvvval  22153  mhpsclcl  22219  psdmul  22238  psdmvr  22241  coe1z  22333  coe1mul2lem1  22337  coe1tm  22343  coe1sclmul  22352  coe1sclmul2  22354  evls1sca  22393  evl1sca  22404  evls1fpws  22439  grpvrinv  22466  mdetunilem9  22687  pttoponconst  23664  cnmptc  23729  cnmptkc  23746  pt1hmeo  23873  tmdgsum2  24163  tsms0  24209  tgptsmscls  24217  resspwsds  24439  imasdsf1olem  24440  nmoeq0  24803  idnghm  24810  rrxcph  25461  ovolctb  25559  ovoliunnul  25576  vitalilem4  25680  vitalilem5  25681  ismbf  25697  mbfconst  25702  mbfss  25715  mbfmulc2re  25717  mbfneg  25719  mbfmulc2  25732  itg11  25760  itg2const  25809  itg2mulclem  25815  itg2mulc  25816  itg2monolem1  25819  itg0  25849  itgz  25850  itgvallem3  25855  iblposlem  25861  i1fibl  25877  itgitg1  25878  itgge0  25880  iblconst  25887  itgconst  25888  itgfsum  25896  iblmulc2  25900  itgmulc2lem1  25901  bddmulibl  25908  bddiblnc  25911  dvcmulf  26014  dvexp  26022  dvexp2  26023  dvmptid  26026  dvmptc  26027  dvef  26049  rolle  26059  dv11cn  26070  ftc1lem4  26108  ftc2  26113  tdeglem4  26127  ply1nzb  26190  plyconst  26273  plyeq0lem  26277  plypf1  26279  coeeulem  26291  plyco  26308  0dgr  26312  0dgrb  26313  dgrcolem2  26341  dgrco  26342  plymul02  26351  plymulidp  26353  plyremlem  26375  elqaalem3  26392  iaa  26396  taylply2  26438  itgulm  26478  amgmlem  27061  lgam1  27135  ftalem7  27150  basellem8  27159  dchrfi  27326  dchrptlem3  27337  istrkg2ld  28636  bra0  32160  padct  32926  cshw1s2  33144  gsumind  33534  mplasclco  33815  selvply1rhmlem2  33820  selvply1rhm0  33825  extvfvcl  33835  mplvrpmmhm  33845  psrgsum  33847  psrmonprod  33851  esplyfval3  33871  fedgmullem2  33929  extdgfialglem2  33992  zar0ring  34177  xrge0mulc1cn  34240  esumnul  34347  esum0  34348  esumcvg  34385  ofcc  34405  mbfmcst  34558  sibf0  34633  0rrv  34750  ccatmulgnn0dir  34841  txsconnlem  35595  cvmliftphtlem  35672  faclim  36101  matunitlindflem1  38120  poimirlem30  38154  ovoliunnfl  38166  voliunnfl  38168  volsupnfl  38169  itg2addnclem  38175  iblmulc2nc  38189  itgmulc2nclem1  38190  itgmulc2nclem2  38191  itgmulc2nc  38192  itgabsnc  38193  ftc1cnnclem  38195  ftc1anclem3  38199  ftc1anclem5  38201  ftc1anclem7  38203  ftc1anclem8  38204  ftc2nc  38206  repwsmet  38338  rrnequiv  38339  fsuppssindlem2  43179  fsuppssind  43180  mzpconstmpt  43326  mzpcompact2lem  43337  mendlmod  43771  mendassa  43772  mnringmulrcld  44809  expgrowthi  44900  expgrowth  44902  binomcxplemrat  44917  binomcxplemnotnn0  44923  climconstmpt  46223  iblconstmpt  46521  iblempty  46530  itgiccshift  46545  itgperiod  46546  itgsbtaddcnst  46547  stoweidlem21  46586  hoicvr  47113  nthrucw  47453  cjnpoly  47474  lindsrng01  49081  eufsn  49454  diag1a  49917  aacllem  50413  amgmlemALT  50415