Theorem fconstmpt 5736

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 4639	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 621	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5212	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5680	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5229	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2764	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 394   = wceq 1534   ∈ wcel 2099  {csn 4623  {copab 5207   ↦ cmpt 5228   × cxp 5672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-sn 4624  df-opab 5208  df-mpt 5229  df-xp 5680

This theorem is referenced by:  fconst  6780  fcoconst  7140  fmptsn  7173  rnmptc  7216  fconstmpo  7534  ofc12  7711  caofinvl  7713  xpexgALT  7987  cantnf  9729  cnfcom2lem  9737  repsconst  14775  harmonic  15858  geomulcvg  15875  vdwlem8  16985  ramcl  17026  pwsvscafval  17504  setcepi  18105  diag2  18265  pws0g  18758  smndex1igid  18889  0frgp  19773  pwsgsum  19976  rrgsupp  20675  lmhmvsca  21019  uvcresum  21787  psrlinv  21960  psrlidm  21967  psrridm  21968  psrass23l  21972  psrass23  21974  mplcoe1  22040  mplcoe3  22041  mplcoe5  22043  mplmon2  22070  evlslem2  22090  evlslem1  22093  mhpsclcl  22137  psdmul  22156  coe1z  22250  coe1mul2lem1  22254  coe1tm  22260  coe1sclmul  22269  coe1sclmul2  22271  evls1sca  22311  evl1sca  22322  evls1fpws  22357  grpvrinv  22387  mdetunilem9  22610  pttoponconst  23589  cnmptc  23654  cnmptkc  23671  pt1hmeo  23798  tmdgsum2  24088  tsms0  24134  tgptsmscls  24142  resspwsds  24366  imasdsf1olem  24367  nmoeq0  24741  idnghm  24748  rrxcph  25408  ovolctb  25507  ovoliunnul  25524  vitalilem4  25628  vitalilem5  25629  ismbf  25645  mbfconst  25650  mbfss  25663  mbfmulc2re  25665  mbfneg  25667  mbfmulc2  25680  itg11  25708  itg2const  25758  itg2mulclem  25764  itg2mulc  25765  itg2monolem1  25768  itg0  25797  itgz  25798  itgvallem3  25803  iblposlem  25809  i1fibl  25825  itgitg1  25826  itgge0  25828  iblconst  25835  itgconst  25836  itgfsum  25844  iblmulc2  25848  itgmulc2lem1  25849  bddmulibl  25856  bddiblnc  25859  dvcmulf  25964  dvexp  25973  dvexp2  25974  dvmptid  25977  dvmptc  25978  dvef  26000  rolle  26010  dv11cn  26022  ftc1lem4  26062  ftc2  26067  tdeglem4  26083  tdeglem4OLD  26084  ply1nzb  26147  plyconst  26230  plyeq0lem  26234  plypf1  26236  coeeulem  26248  plyco  26265  0dgr  26269  0dgrb  26270  dgrcolem2  26299  dgrco  26300  plyremlem  26329  elqaalem3  26346  iaa  26350  taylply2  26392  taylply2OLD  26393  itgulm  26434  amgmlem  27015  lgam1  27089  ftalem7  27104  basellem8  27113  dchrfi  27281  dchrptlem3  27292  bra0  31880  padct  32633  cshw1s2  32827  fedgmullem2  33531  zar0ring  33706  xrge0mulc1cn  33769  esumnul  33894  esum0  33895  esumcvg  33932  ofcc  33952  mbfmcst  34106  sibf0  34181  0rrv  34298  ccatmulgnn0dir  34401  plymul02  34405  plymulx  34407  txsconnlem  35081  cvmliftphtlem  35158  faclim  35581  matunitlindflem1  37330  poimirlem30  37364  ovoliunnfl  37376  voliunnfl  37378  volsupnfl  37379  itg2addnclem  37385  iblmulc2nc  37399  itgmulc2nclem1  37400  itgmulc2nclem2  37401  itgmulc2nc  37402  itgabsnc  37403  ftc1cnnclem  37405  ftc1anclem3  37409  ftc1anclem5  37411  ftc1anclem7  37413  ftc1anclem8  37414  ftc2nc  37416  repwsmet  37548  rrnequiv  37549  evlsvvval  42253  fsuppssindlem2  42282  fsuppssind  42283  mzpconstmpt  42434  mzpcompact2lem  42445  mendlmod  42891  mendassa  42892  mnringmulrcld  43939  expgrowthi  44044  expgrowth  44046  binomcxplemrat  44061  binomcxplemnotnn0  44067  climconstmpt  45315  iblconstmpt  45613  iblempty  45622  itgiccshift  45637  itgperiod  45638  itgsbtaddcnst  45639  stoweidlem21  45678  lindsrng01  47887  eufsn  48245  aacllem  48585  amgmlemALT  48587