Theorem fconstmpt 5722

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 4604	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 634	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5177	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5666	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5192	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2795	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

This proof depends on syntax axioms:   ∧ wa 400   = wceq 1569   ∈ wcel 2142  {csn 4588  {copab 5172   ↦ cmpt 5191   × cxp 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-sn 4589  df-opab 5173  df-mpt 5192  df-xp 5666

This theorem is used by:  fconst  6764  fcoconst  7130  fmptsn  7165  rnmptc  7205  fconstmpo  7529  ofc12  7706  caofinvl  7708  caofidlcan  7714  xpexgALT  7976  cantnf  9660  cnfcom2lem  9668  repsconst  14816  harmonic  15920  geomulcvg  15937  vdwlem8  17054  ramcl  17095  pwsvscafval  17554  setcepi  18151  diag2  18307  pws0g  18837  smndex1gbas  18967  smndex1gid  18969  smndex1igid  18971  smndex1igidOLD  18972  0frgp  19855  pwsgsum  20058  rrgsupp  20811  lmhmvsca  21177  uvcresum  21954  psrlinv  22116  psrlidm  22122  psrridm  22123  psrass23l  22127  psrass23  22129  mplcoe1  22199  mplcoe3  22200  mplcoe5  22202  mplmon2  22223  evlslem2  22241  evlslem1  22244  evlsvvval  22255  mhpsclcl  22321  psdmul  22340  psdmvr  22343  coe1z  22435  coe1mul2lem1  22439  coe1tm  22445  coe1sclmul  22454  coe1sclmul2  22456  evls1sca  22494  evl1sca  22505  evls1fpws  22540  grpvrinv  22567  mdetunilem9  22788  pttoponconst  23765  cnmptc  23830  cnmptkc  23847  pt1hmeo  23974  tmdgsum2  24264  tsms0  24310  tgptsmscls  24318  resspwsds  24540  imasdsf1olem  24541  nmoeq0  24904  idnghm  24911  rrxcph  25562  ovolctb  25660  ovoliunnul  25677  vitalilem4  25781  vitalilem5  25782  ismbf  25798  mbfconst  25803  mbfss  25816  mbfmulc2re  25818  mbfneg  25820  mbfmulc2  25833  itg11  25861  itg2const  25910  itg2mulclem  25916  itg2mulc  25917  itg2monolem1  25920  itg0  25950  itgz  25951  itgvallem3  25956  iblposlem  25962  i1fibl  25978  itgitg1  25979  itgge0  25981  iblconst  25988  itgconst  25989  itgfsum  25997  iblmulc2  26001  itgmulc2lem1  26002  bddmulibl  26009  bddiblnc  26012  dvcmulf  26115  dvexp  26123  dvexp2  26124  dvmptid  26127  dvmptc  26128  dvef  26150  rolle  26160  dv11cn  26171  ftc1lem4  26209  ftc2  26214  tdeglem4  26228  ply1nzb  26291  plyconst  26374  plyeq0lem  26378  plypf1  26380  coeeulem  26392  plyco  26409  0dgr  26413  0dgrb  26414  dgrcolem2  26442  dgrco  26443  plymul02  26452  plymulidp  26454  plyremlem  26476  elqaalem3  26493  iaa  26499  taylply2  26542  itgulm  26582  amgmlem  27165  lgam1  27239  ftalem7  27254  basellem8  27263  dchrfi  27430  dchrptlem3  27441  istrkg2ld  28740  bra0  32313  padct  33074  cshw1s2  33289  gsumind  33674  mplasclco  33915  selvply1rhmlem2  33920  selvply1rhm0  33925  extvfvcl  33935  mplvrpmmhm  33945  psrgsum  33947  psrmonprod  33951  esplyfval3  33971  fedgmullem2  34029  extdgfialglem2  34092  zar0ring  34277  xrge0mulc1cn  34340  esumnul  34447  esum0  34448  esumcvg  34485  ofcc  34505  mbfmcst  34658  sibf0  34733  0rrv  34850  ccatmulgnn0dir  34941  txsconnlem  35740  cvmliftphtlem  35817  faclim  36246  matunitlindflem1  38295  poimirlem30  38329  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  itg2addnclem  38350  iblmulc2nc  38364  itgmulc2nclem1  38365  itgmulc2nclem2  38366  itgmulc2nc  38367  itgabsnc  38368  ftc1cnnclem  38370  ftc1anclem3  38374  ftc1anclem5  38376  ftc1anclem7  38378  ftc1anclem8  38379  ftc2nc  38381  repwsmet  38513  rrnequiv  38514  fsuppssindlem2  43352  fsuppssind  43353  mzpconstmpt  43499  mzpcompact2lem  43510  mendlmod  43944  mendassa  43945  mnringmulrcld  44980  expgrowthi  45071  expgrowth  45073  binomcxplemrat  45088  binomcxplemnotnn0  45094  climconstmpt  46400  iblconstmpt  46698  iblempty  46707  itgiccshift  46722  itgperiod  46723  itgsbtaddcnst  46724  stoweidlem21  46763  hoicvr  47290  cjnpoly  47654  lindsrng01  49276  eufsn  49648  diag1a  50111  aacllem  50649  amgmlemALT  50678