Theorem fconstmpt 5717

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {csn 4588  {copab 5170   ↦ cmpt 5189   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-sn 4589  df-opab 5171  df-mpt 5190  df-xp 5661

This theorem is used by:  fconst  6790  fcoconst  7159  fmptsn  7195  rnmptc  7236  fconstmpo  7560  ofc12  7747  caofinvl  7749  caofidlcan  7755  xpexgALT  8017  cantnf  9721  cnfcom2lem  9729  repsconst  14951  harmonic  16057  geomulcvg  16074  vdwlem8  17195  ramcl  17236  pwsvscafval  17695  setcepi  18292  diag2  18448  pws0g  18996  smndex1gbas  19127  smndex1gid  19129  smndex1igid  19131  smndex1igidOLD  19132  0frgp  20023  pwsgsum  20226  rrgsupp  20983  lmhmvsca  21350  uvcresum  22129  psrlinv  22293  psrlidm  22299  psrridm  22300  psrass23l  22304  psrass23  22306  mplcoe1  22376  mplcoe3  22377  mplcoe5  22379  mplmon2  22400  evlslem2  22418  evlslem1  22421  evlsvvval  22432  mhpsclcl  22498  psdmul  22517  psdmvr  22520  coe1z  22612  coe1mul2lem1  22616  coe1tm  22622  coe1sclmul  22631  coe1sclmul2  22633  evls1sca  22671  evl1sca  22682  evls1fpws  22717  grpvrinv  22744  mdetunilem9  22965  matunitlindflem1  23024  pttoponconst  23946  cnmptc  24011  cnmptkc  24028  pt1hmeo  24155  tmdgsum2  24445  tsms0  24491  tgptsmscls  24499  resspwsds  24721  imasdsf1olem  24722  nmoeq0  25085  idnghm  25092  rrxcph  25743  ovolctb  25841  ovoliunnul  25858  vitalilem4  25962  vitalilem5  25963  ismbf  25979  mbfconst  25984  mbfss  25997  mbfmulc2re  25999  mbfneg  26001  mbfmulc2  26014  itg11  26042  itg2const  26091  itg2mulclem  26097  itg2mulc  26098  itg2monolem1  26101  itg0  26130  itgz  26131  itgvallem3  26136  iblposlem  26142  i1fibl  26158  itgitg1  26159  itgge0  26161  iblconst  26168  itgconst  26169  itgfsum  26177  iblmulc2  26181  itgmulc2lem1  26182  bddmulibl  26189  bddiblnc  26192  dvcmulf  26295  dvexp  26303  dvexp2  26304  dvmptid  26307  dvmptc  26308  dvef  26330  rolle  26340  dv11cn  26351  ftc1lem4  26389  ftc2  26394  tdeglem4  26408  ply1nzb  26471  plyconst  26554  plyeq0lem  26559  plypf1  26561  coeeulem  26573  plyco  26590  0dgr  26594  0dgrb  26595  dgrcolem2  26623  dgrco  26624  plymul02  26631  plymulidp  26633  plyremlem  26655  elqaalem3  26674  iaaOLD  26682  taylply2  26725  itgulm  26765  amgmlem  27347  lgam1  27421  ftalem7  27436  basellem8  27445  dchrfi  27612  dchrptlem3  27623  istrkg2ld  28952  bra0  32582  padct  33381  cshw1s2  33591  gsumind  33976  mplasclco  34218  selvply1rhmlem2  34223  selvply1rhm0  34228  extvfvcl  34238  mplvrpmmhm  34248  psrgsum  34250  psrmonprod  34254  esplyfval3  34274  fedgmullem2  34332  extdgfialglem2  34395  zar0ring  34580  xrge0mulc1cn  34643  esumnul  34750  esum0  34751  esumcvg  34788  ofcc  34808  mbfmcst  34961  sibf0  35036  0rrv  35153  ccatmulgnn0dir  35244  txsconnlem  36172  cvmliftphtlem  36249  faclim  36689  poimirlem30  38760  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  itg2addnclem  38781  iblmulc2nc  38795  itgmulc2nclem1  38796  itgmulc2nclem2  38797  itgmulc2nc  38798  itgabsnc  38799  ftc1cnnclem  38801  ftc1anclem3  38805  ftc1anclem5  38807  ftc1anclem7  38809  ftc1anclem8  38810  ftc2nc  38812  repwsmet  38960  rrnequiv  38961  fsuppssindlem2  43813  fsuppssind  43814  mzpconstmpt  43944  mzpcompact2lem  43955  mendlmod  44383  mendassa  44384  mnringmulrcld  45418  expgrowthi  45509  expgrowth  45511  binomcxplemrat  45526  binomcxplemnotnn0  45532  climconstmpt  46873  iblconstmpt  47171  iblempty  47180  itgiccshift  47195  itgperiod  47196  itgsbtaddcnst  47197  stoweidlem21  47236  hoicvr  47763  cjnpoly  48144  lindsrng01  49785  eufsn  50158  diag1a  50632  aacllem  51219  veroquadmodzerod  51264  amgmlemALT  51268