Theorem fconstmpt 5596

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 4543	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 626	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5106	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5542	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5121	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2769	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 399   = wceq 1543   ∈ wcel 2112  {csn 4527  {copab 5101   ↦ cmpt 5120   × cxp 5534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-sn 4528  df-opab 5102  df-mpt 5121  df-xp 5542

This theorem is referenced by:  fconst  6583  fcoconst  6927  fmptsn  6960  rnmptc  7000  rnmptcOLD  7001  fconstmpo  7305  ofc12  7474  caofinvl  7476  xpexgALT  7732  cantnf  9286  cnfcom2lem  9294  repsconst  14302  harmonic  15386  geomulcvg  15403  vdwlem8  16504  ramcl  16545  pwsvscafval  16953  setcepi  17548  diag2  17707  pws0g  18163  smndex1igid  18285  0frgp  19123  pwsgsum  19321  lmhmvsca  20036  rrgsupp  20283  uvcresum  20709  psrlinv  20876  psrlidm  20882  psrridm  20883  psrass23l  20887  psrass23  20889  mplcoe1  20948  mplcoe3  20949  mplcoe5  20951  mplmon2  20973  evlslem2  20993  evlslem1  20996  mhpsclcl  21041  coe1z  21138  coe1mul2lem1  21142  coe1tm  21148  coe1sclmul  21157  coe1sclmul2  21159  evls1sca  21193  evl1sca  21204  grpvrinv  21249  mdetunilem9  21471  pttoponconst  22448  cnmptc  22513  cnmptkc  22530  pt1hmeo  22657  tmdgsum2  22947  tsms0  22993  tgptsmscls  23001  resspwsds  23224  imasdsf1olem  23225  nmoeq0  23588  idnghm  23595  rrxcph  24243  ovolctb  24341  ovoliunnul  24358  vitalilem4  24462  vitalilem5  24463  ismbf  24479  mbfconst  24484  mbfss  24497  mbfmulc2re  24499  mbfneg  24501  mbfmulc2  24514  itg11  24542  itg2const  24592  itg2mulclem  24598  itg2mulc  24599  itg2monolem1  24602  itg0  24631  itgz  24632  itgvallem3  24637  iblposlem  24643  i1fibl  24659  itgitg1  24660  itgge0  24662  iblconst  24669  itgconst  24670  itgfsum  24678  iblmulc2  24682  itgmulc2lem1  24683  bddmulibl  24690  bddiblnc  24693  dvcmulf  24796  dvexp  24804  dvexp2  24805  dvmptid  24808  dvmptc  24809  dvef  24831  rolle  24841  dv11cn  24852  ftc1lem4  24890  ftc2  24895  tdeglem4  24911  tdeglem4OLD  24912  ply1nzb  24974  plyconst  25054  plyeq0lem  25058  plypf1  25060  coeeulem  25072  plyco  25089  0dgr  25093  0dgrb  25094  dgrcolem2  25122  dgrco  25123  plyremlem  25151  elqaalem3  25168  iaa  25172  taylply2  25214  itgulm  25254  amgmlem  25826  lgam1  25900  ftalem7  25915  basellem8  25924  dchrfi  26090  dchrptlem3  26101  bra0  29985  padct  30728  cshw1s2  30906  fedgmullem2  31379  zar0ring  31496  xrge0mulc1cn  31559  esumnul  31682  esum0  31683  esumcvg  31720  ofcc  31740  mbfmcst  31892  sibf0  31967  0rrv  32084  ccatmulgnn0dir  32187  plymul02  32191  plymulx  32193  txsconnlem  32869  cvmliftphtlem  32946  faclim  33381  matunitlindflem1  35459  poimirlem30  35493  ovoliunnfl  35505  voliunnfl  35507  volsupnfl  35508  itg2addnclem  35514  iblmulc2nc  35528  itgmulc2nclem1  35529  itgmulc2nclem2  35530  itgmulc2nc  35531  itgabsnc  35532  ftc1cnnclem  35534  ftc1anclem3  35538  ftc1anclem5  35540  ftc1anclem7  35542  ftc1anclem8  35543  ftc2nc  35545  repwsmet  35678  rrnequiv  35679  evlsbagval  39926  fsuppssindlem2  39932  fsuppssind  39933  mzpconstmpt  40206  mzpcompact2lem  40217  mendlmod  40662  mendassa  40663  mnringmulrcld  41460  expgrowthi  41565  expgrowth  41567  binomcxplemrat  41582  binomcxplemnotnn0  41588  climconstmpt  42817  iblconstmpt  43115  iblempty  43124  itgiccshift  43139  itgperiod  43140  itgsbtaddcnst  43141  stoweidlem21  43180  lindsrng01  45425  eufsn  45785  aacllem  46119  amgmlemALT  46121