Theorem fconstmpt 5614

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

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {csn 4567  {copab 5128   ↦ cmpt 5146   × cxp 5553

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-sn 4568  df-opab 5129  df-mpt 5147  df-xp 5561

This theorem is referenced by:  fconst  6565  fcoconst  6896  fmptsn  6929  rnmptc  6969  rnmptcOLD  6970  fconstmpo  7269  ofc12  7434  caofinvl  7436  xpexgALT  7682  cantnf  9156  cnfcom2lem  9164  repsconst  14134  harmonic  15214  geomulcvg  15232  vdwlem8  16324  ramcl  16365  pwsvscafval  16767  setcepi  17348  diag2  17495  pws0g  17947  smndex1igid  18069  0frgp  18905  pwsgsum  19102  lmhmvsca  19817  rrgsupp  20064  psrlinv  20177  psrlidm  20183  psrridm  20184  psrass23l  20188  psrass23  20190  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  mplmon2  20273  evlslem2  20292  evlslem1  20295  coe1z  20431  coe1mul2lem1  20435  coe1tm  20441  coe1sclmul  20450  coe1sclmul2  20452  evls1sca  20486  evl1sca  20497  uvcresum  20937  grpvrinv  21007  mdetunilem9  21229  pttoponconst  22205  cnmptc  22270  cnmptkc  22287  pt1hmeo  22414  tmdgsum2  22704  tsms0  22750  tgptsmscls  22758  resspwsds  22982  imasdsf1olem  22983  nmoeq0  23345  idnghm  23352  rrxcph  23995  ovolctb  24091  ovoliunnul  24108  vitalilem4  24212  vitalilem5  24213  ismbf  24229  mbfconst  24234  mbfss  24247  mbfmulc2re  24249  mbfneg  24251  mbfmulc2  24264  itg11  24292  itg2const  24341  itg2mulclem  24347  itg2mulc  24348  itg2monolem1  24351  itg0  24380  itgz  24381  itgvallem3  24386  iblposlem  24392  i1fibl  24408  itgitg1  24409  itgge0  24411  iblconst  24418  itgconst  24419  itgfsum  24427  iblmulc2  24431  itgmulc2lem1  24432  bddmulibl  24439  dvcmulf  24542  dvexp  24550  dvexp2  24551  dvmptid  24554  dvmptc  24555  dvef  24577  rolle  24587  dv11cn  24598  ftc1lem4  24636  ftc2  24641  tdeglem4  24654  ply1nzb  24716  plyconst  24796  plyeq0lem  24800  plypf1  24802  coeeulem  24814  plyco  24831  0dgr  24835  0dgrb  24836  dgrcolem2  24864  dgrco  24865  plyremlem  24893  elqaalem3  24910  iaa  24914  taylply2  24956  itgulm  24996  amgmlem  25567  lgam1  25641  ftalem7  25656  basellem8  25665  dchrfi  25831  dchrptlem3  25842  bra0  29727  padct  30455  cshw1s2  30634  fedgmullem2  31026  xrge0mulc1cn  31184  esumnul  31307  esum0  31308  esumcvg  31345  ofcc  31365  mbfmcst  31517  sibf0  31592  0rrv  31709  ccatmulgnn0dir  31812  plymul02  31816  plymulx  31818  txsconnlem  32487  cvmliftphtlem  32564  faclim  32978  matunitlindflem1  34903  poimirlem30  34937  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  itg2addnclem  34958  iblmulc2nc  34972  itgmulc2nclem1  34973  itgmulc2nclem2  34974  itgmulc2nc  34975  itgabsnc  34976  bddiblnc  34977  ftc1cnnclem  34980  ftc1anclem3  34984  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anclem8  34989  ftc2nc  34991  repwsmet  35127  rrnequiv  35128  mzpconstmpt  39357  mzpcompact2lem  39368  mendlmod  39813  mendassa  39814  expgrowthi  40685  expgrowth  40687  binomcxplemrat  40702  binomcxplemnotnn0  40708  climconstmpt  41959  iblconstmpt  42261  iblempty  42270  itgiccshift  42285  itgperiod  42286  itgsbtaddcnst  42287  stoweidlem21  42326  lindsrng01  44543  aacllem  44922  amgmlemALT  44924