Theorem fconstmpt 5676

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2110  {csn 4574  {copab 5151   ↦ cmpt 5170   × cxp 5612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-sn 4575  df-opab 5152  df-mpt 5171  df-xp 5620

This theorem is referenced by:  fconst  6705  fcoconst  7062  fmptsn  7096  rnmptc  7136  fconstmpo  7458  ofc12  7635  caofinvl  7637  caofidlcan  7643  xpexgALT  7908  cantnf  9578  cnfcom2lem  9586  repsconst  14671  harmonic  15758  geomulcvg  15775  vdwlem8  16892  ramcl  16933  pwsvscafval  17390  setcepi  17987  diag2  18143  pws0g  18673  smndex1igid  18804  0frgp  19684  pwsgsum  19887  rrgsupp  20609  lmhmvsca  20972  uvcresum  21723  psrlinv  21885  psrlidm  21892  psrridm  21893  psrass23l  21897  psrass23  21899  mplcoe1  21965  mplcoe3  21966  mplcoe5  21968  mplmon2  21989  evlslem2  22007  evlslem1  22010  mhpsclcl  22055  psdmul  22074  psdmvr  22077  coe1z  22170  coe1mul2lem1  22174  coe1tm  22180  coe1sclmul  22189  coe1sclmul2  22191  evls1sca  22231  evl1sca  22242  evls1fpws  22277  grpvrinv  22307  mdetunilem9  22528  pttoponconst  23505  cnmptc  23570  cnmptkc  23587  pt1hmeo  23714  tmdgsum2  24004  tsms0  24050  tgptsmscls  24058  resspwsds  24280  imasdsf1olem  24281  nmoeq0  24644  idnghm  24651  rrxcph  25312  ovolctb  25411  ovoliunnul  25428  vitalilem4  25532  vitalilem5  25533  ismbf  25549  mbfconst  25554  mbfss  25567  mbfmulc2re  25569  mbfneg  25571  mbfmulc2  25584  itg11  25612  itg2const  25661  itg2mulclem  25667  itg2mulc  25668  itg2monolem1  25671  itg0  25701  itgz  25702  itgvallem3  25707  iblposlem  25713  i1fibl  25729  itgitg1  25730  itgge0  25732  iblconst  25739  itgconst  25740  itgfsum  25748  iblmulc2  25752  itgmulc2lem1  25753  bddmulibl  25760  bddiblnc  25763  dvcmulf  25868  dvexp  25877  dvexp2  25878  dvmptid  25881  dvmptc  25882  dvef  25904  rolle  25914  dv11cn  25926  ftc1lem4  25966  ftc2  25971  tdeglem4  25985  ply1nzb  26048  plyconst  26131  plyeq0lem  26135  plypf1  26137  coeeulem  26149  plyco  26166  0dgr  26170  0dgrb  26171  dgrcolem2  26200  dgrco  26201  plyremlem  26232  elqaalem3  26249  iaa  26253  taylply2  26295  taylply2OLD  26296  itgulm  26337  amgmlem  26920  lgam1  26994  ftalem7  27009  basellem8  27018  dchrfi  27186  dchrptlem3  27197  bra0  31920  padct  32691  cshw1s2  32931  gsumind  33300  mplvrpmmhm  33566  fedgmullem2  33633  extdgfialglem2  33696  zar0ring  33881  xrge0mulc1cn  33944  esumnul  34051  esum0  34052  esumcvg  34089  ofcc  34109  mbfmcst  34262  sibf0  34337  0rrv  34454  ccatmulgnn0dir  34545  plymul02  34549  plymulx  34551  txsconnlem  35252  cvmliftphtlem  35329  faclim  35758  matunitlindflem1  37635  poimirlem30  37669  ovoliunnfl  37681  voliunnfl  37683  volsupnfl  37684  itg2addnclem  37690  iblmulc2nc  37704  itgmulc2nclem1  37705  itgmulc2nclem2  37706  itgmulc2nc  37707  itgabsnc  37708  ftc1cnnclem  37710  ftc1anclem3  37714  ftc1anclem5  37716  ftc1anclem7  37718  ftc1anclem8  37719  ftc2nc  37721  repwsmet  37853  rrnequiv  37854  evlsvvval  42575  fsuppssindlem2  42604  fsuppssind  42605  mzpconstmpt  42752  mzpcompact2lem  42763  mendlmod  43201  mendassa  43202  mnringmulrcld  44240  expgrowthi  44345  expgrowth  44347  binomcxplemrat  44362  binomcxplemnotnn0  44368  climconstmpt  45675  iblconstmpt  45973  iblempty  45982  itgiccshift  45997  itgperiod  45998  itgsbtaddcnst  45999  stoweidlem21  46038  cjnpoly  46899  lindsrng01  48479  eufsn  48852  diag1a  49316  aacllem  49812  amgmlemALT  49814