Theorem fconstmpt 5698

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 4588	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 631	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5157	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5642	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5172	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2785	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 398   = wceq 1550   ∈ wcel 2132  {csn 4572  {copab 5152   ↦ cmpt 5171   × cxp 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-sn 4573  df-opab 5153  df-mpt 5172  df-xp 5642

This theorem is referenced by:  fconst  6735  fcoconst  7101  fmptsn  7136  rnmptc  7176  fconstmpo  7498  ofc12  7675  caofinvl  7677  caofidlcan  7683  xpexgALT  7947  cantnf  9634  cnfcom2lem  9642  repsconst  14771  harmonic  15861  geomulcvg  15878  vdwlem8  16996  ramcl  17037  pwsvscafval  17496  setcepi  18093  diag2  18249  pws0g  18779  smndex1gbas  18908  smndex1gid  18910  smndex1igid  18912  smndex1igidOLD  18913  0frgp  19791  pwsgsum  19994  rrgsupp  20719  lmhmvsca  21081  uvcresum  21814  psrlinv  21976  psrlidm  21982  psrridm  21983  psrass23l  21987  psrass23  21989  mplcoe1  22059  mplcoe3  22060  mplcoe5  22062  mplmon2  22083  evlslem2  22101  evlslem1  22104  evlsvvval  22115  mhpsclcl  22181  psdmul  22200  psdmvr  22203  coe1z  22295  coe1mul2lem1  22299  coe1tm  22305  coe1sclmul  22314  coe1sclmul2  22316  evls1sca  22355  evl1sca  22366  evls1fpws  22401  grpvrinv  22428  mdetunilem9  22649  pttoponconst  23626  cnmptc  23691  cnmptkc  23708  pt1hmeo  23835  tmdgsum2  24125  tsms0  24171  tgptsmscls  24179  resspwsds  24401  imasdsf1olem  24402  nmoeq0  24765  idnghm  24772  rrxcph  25423  ovolctb  25521  ovoliunnul  25538  vitalilem4  25642  vitalilem5  25643  ismbf  25659  mbfconst  25664  mbfss  25677  mbfmulc2re  25679  mbfneg  25681  mbfmulc2  25694  itg11  25722  itg2const  25771  itg2mulclem  25777  itg2mulc  25778  itg2monolem1  25781  itg0  25811  itgz  25812  itgvallem3  25817  iblposlem  25823  i1fibl  25839  itgitg1  25840  itgge0  25842  iblconst  25849  itgconst  25850  itgfsum  25858  iblmulc2  25862  itgmulc2lem1  25863  bddmulibl  25870  bddiblnc  25873  dvcmulf  25976  dvexp  25984  dvexp2  25985  dvmptid  25988  dvmptc  25989  dvef  26011  rolle  26021  dv11cn  26032  ftc1lem4  26070  ftc2  26075  tdeglem4  26089  ply1nzb  26152  plyconst  26235  plyeq0lem  26239  plypf1  26241  coeeulem  26253  plyco  26270  0dgr  26274  0dgrb  26275  dgrcolem2  26303  dgrco  26304  plyremlem  26334  elqaalem3  26351  iaa  26355  taylply2  26397  itgulm  26437  amgmlem  27020  lgam1  27094  ftalem7  27109  basellem8  27118  dchrfi  27285  dchrptlem3  27296  istrkg2ld  28595  bra0  32088  padct  32859  cshw1s2  33088  gsumind  33477  mplasclco  33757  selvply1rhmlem2  33762  selvply1rhm0  33767  extvfvcl  33777  mplvrpmmhm  33787  psrgsum  33789  psrmonprod  33793  esplyfval3  33813  fedgmullem2  33871  extdgfialglem2  33934  zar0ring  34119  xrge0mulc1cn  34182  esumnul  34289  esum0  34290  esumcvg  34327  ofcc  34347  mbfmcst  34500  sibf0  34575  0rrv  34692  ccatmulgnn0dir  34783  plymul02  34787  plymulx  34789  txsconnlem  35528  cvmliftphtlem  35605  faclim  36034  matunitlindflem1  38053  poimirlem30  38087  ovoliunnfl  38099  voliunnfl  38101  volsupnfl  38102  itg2addnclem  38108  iblmulc2nc  38122  itgmulc2nclem1  38123  itgmulc2nclem2  38124  itgmulc2nc  38125  itgabsnc  38126  ftc1cnnclem  38128  ftc1anclem3  38132  ftc1anclem5  38134  ftc1anclem7  38136  ftc1anclem8  38137  ftc2nc  38139  repwsmet  38271  rrnequiv  38272  fsuppssindlem2  43112  fsuppssind  43113  mzpconstmpt  43259  mzpcompact2lem  43270  mendlmod  43704  mendassa  43705  mnringmulrcld  44742  expgrowthi  44847  expgrowth  44849  binomcxplemrat  44864  binomcxplemnotnn0  44870  climconstmpt  46170  iblconstmpt  46468  iblempty  46477  itgiccshift  46492  itgperiod  46493  itgsbtaddcnst  46494  stoweidlem21  46533  hoicvr  47060  nthrucw  47400  cjnpoly  47421  lindsrng01  49028  eufsn  49401  diag1a  49864  aacllem  50360  amgmlemALT  50362