Theorem fconstmpt 5684

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4568  {copab 5148   ↦ cmpt 5167   × cxp 5620

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 3432  df-sn 4569  df-opab 5149  df-mpt 5168  df-xp 5628

This theorem is referenced by:  fconst  6718  fcoconst  7079  fmptsn  7113  rnmptc  7153  fconstmpo  7475  ofc12  7652  caofinvl  7654  caofidlcan  7660  xpexgALT  7925  cantnf  9603  cnfcom2lem  9611  repsconst  14696  harmonic  15783  geomulcvg  15800  vdwlem8  16917  ramcl  16958  pwsvscafval  17416  setcepi  18013  diag2  18169  pws0g  18699  smndex1gbas  18828  smndex1gid  18830  smndex1igid  18832  smndex1igidOLD  18833  0frgp  19712  pwsgsum  19915  rrgsupp  20636  lmhmvsca  20999  uvcresum  21750  psrlinv  21912  psrlidm  21918  psrridm  21919  psrass23l  21923  psrass23  21925  mplcoe1  21993  mplcoe3  21994  mplcoe5  21996  mplmon2  22017  evlslem2  22035  evlslem1  22038  evlsvvval  22049  mhpsclcl  22091  psdmul  22110  psdmvr  22113  coe1z  22206  coe1mul2lem1  22210  coe1tm  22216  coe1sclmul  22225  coe1sclmul2  22227  evls1sca  22266  evl1sca  22277  evls1fpws  22312  grpvrinv  22342  mdetunilem9  22563  pttoponconst  23540  cnmptc  23605  cnmptkc  23622  pt1hmeo  23749  tmdgsum2  24039  tsms0  24085  tgptsmscls  24093  resspwsds  24315  imasdsf1olem  24316  nmoeq0  24679  idnghm  24686  rrxcph  25337  ovolctb  25435  ovoliunnul  25452  vitalilem4  25556  vitalilem5  25557  ismbf  25573  mbfconst  25578  mbfss  25591  mbfmulc2re  25593  mbfneg  25595  mbfmulc2  25608  itg11  25636  itg2const  25685  itg2mulclem  25691  itg2mulc  25692  itg2monolem1  25695  itg0  25725  itgz  25726  itgvallem3  25731  iblposlem  25737  i1fibl  25753  itgitg1  25754  itgge0  25756  iblconst  25763  itgconst  25764  itgfsum  25772  iblmulc2  25776  itgmulc2lem1  25777  bddmulibl  25784  bddiblnc  25787  dvcmulf  25890  dvexp  25898  dvexp2  25899  dvmptid  25902  dvmptc  25903  dvef  25925  rolle  25935  dv11cn  25947  ftc1lem4  25987  ftc2  25992  tdeglem4  26006  ply1nzb  26069  plyconst  26152  plyeq0lem  26156  plypf1  26158  coeeulem  26170  plyco  26187  0dgr  26191  0dgrb  26192  dgrcolem2  26220  dgrco  26221  plyremlem  26252  elqaalem3  26269  iaa  26273  taylply2  26315  taylply2OLD  26316  itgulm  26357  amgmlem  26940  lgam1  27014  ftalem7  27029  basellem8  27038  dchrfi  27206  dchrptlem3  27217  istrkg2ld  28516  bra0  32010  padct  32780  cshw1s2  33025  gsumind  33410  extvfvcl  33685  mplvrpmmhm  33695  psrgsum  33697  psrmonprod  33701  esplyfval3  33721  fedgmullem2  33780  extdgfialglem2  33843  zar0ring  34028  xrge0mulc1cn  34091  esumnul  34198  esum0  34199  esumcvg  34236  ofcc  34256  mbfmcst  34409  sibf0  34484  0rrv  34601  ccatmulgnn0dir  34692  plymul02  34696  plymulx  34698  txsconnlem  35428  cvmliftphtlem  35505  faclim  35934  matunitlindflem1  37928  poimirlem30  37962  ovoliunnfl  37974  voliunnfl  37976  volsupnfl  37977  itg2addnclem  37983  iblmulc2nc  37997  itgmulc2nclem1  37998  itgmulc2nclem2  37999  itgmulc2nc  38000  itgabsnc  38001  ftc1cnnclem  38003  ftc1anclem3  38007  ftc1anclem5  38009  ftc1anclem7  38011  ftc1anclem8  38012  ftc2nc  38014  repwsmet  38146  rrnequiv  38147  fsuppssindlem2  43024  fsuppssind  43025  mzpconstmpt  43171  mzpcompact2lem  43182  mendlmod  43620  mendassa  43621  mnringmulrcld  44658  expgrowthi  44763  expgrowth  44765  binomcxplemrat  44780  binomcxplemnotnn0  44786  climconstmpt  46090  iblconstmpt  46388  iblempty  46397  itgiccshift  46412  itgperiod  46413  itgsbtaddcnst  46414  stoweidlem21  46453  hoicvr  46980  nthrucw  47318  cjnpoly  47323  lindsrng01  48902  eufsn  49275  diag1a  49738  aacllem  50234  amgmlemALT  50236