Theorem fconstmpt 5693

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4568  {copab 5148   ↦ cmpt 5167   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-sn 4569  df-opab 5149  df-mpt 5168  df-xp 5637

This theorem is referenced by:  fconst  6727  fcoconst  7088  fmptsn  7122  rnmptc  7162  fconstmpo  7484  ofc12  7661  caofinvl  7663  caofidlcan  7669  xpexgALT  7934  cantnf  9614  cnfcom2lem  9622  repsconst  14734  harmonic  15824  geomulcvg  15841  vdwlem8  16959  ramcl  17000  pwsvscafval  17458  setcepi  18055  diag2  18211  pws0g  18741  smndex1gbas  18870  smndex1gid  18872  smndex1igid  18874  smndex1igidOLD  18875  0frgp  19754  pwsgsum  19957  rrgsupp  20678  lmhmvsca  21040  uvcresum  21773  psrlinv  21934  psrlidm  21940  psrridm  21941  psrass23l  21945  psrass23  21947  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  mplmon2  22039  evlslem2  22057  evlslem1  22060  evlsvvval  22071  mhpsclcl  22113  psdmul  22132  psdmvr  22135  coe1z  22228  coe1mul2lem1  22232  coe1tm  22238  coe1sclmul  22247  coe1sclmul2  22249  evls1sca  22288  evl1sca  22299  evls1fpws  22334  grpvrinv  22364  mdetunilem9  22585  pttoponconst  23562  cnmptc  23627  cnmptkc  23644  pt1hmeo  23771  tmdgsum2  24061  tsms0  24107  tgptsmscls  24115  resspwsds  24337  imasdsf1olem  24338  nmoeq0  24701  idnghm  24708  rrxcph  25359  ovolctb  25457  ovoliunnul  25474  vitalilem4  25578  vitalilem5  25579  ismbf  25595  mbfconst  25600  mbfss  25613  mbfmulc2re  25615  mbfneg  25617  mbfmulc2  25630  itg11  25658  itg2const  25707  itg2mulclem  25713  itg2mulc  25714  itg2monolem1  25717  itg0  25747  itgz  25748  itgvallem3  25753  iblposlem  25759  i1fibl  25775  itgitg1  25776  itgge0  25778  iblconst  25785  itgconst  25786  itgfsum  25794  iblmulc2  25798  itgmulc2lem1  25799  bddmulibl  25806  bddiblnc  25809  dvcmulf  25912  dvexp  25920  dvexp2  25921  dvmptid  25924  dvmptc  25925  dvef  25947  rolle  25957  dv11cn  25968  ftc1lem4  26006  ftc2  26011  tdeglem4  26025  ply1nzb  26088  plyconst  26171  plyeq0lem  26175  plypf1  26177  coeeulem  26189  plyco  26206  0dgr  26210  0dgrb  26211  dgrcolem2  26239  dgrco  26240  plyremlem  26270  elqaalem3  26287  iaa  26291  taylply2  26333  itgulm  26373  amgmlem  26953  lgam1  27027  ftalem7  27042  basellem8  27051  dchrfi  27218  dchrptlem3  27229  istrkg2ld  28528  bra0  32021  padct  32791  cshw1s2  33020  gsumind  33405  extvfvcl  33680  mplvrpmmhm  33690  psrgsum  33692  psrmonprod  33696  esplyfval3  33716  fedgmullem2  33774  extdgfialglem2  33837  zar0ring  34022  xrge0mulc1cn  34085  esumnul  34192  esum0  34193  esumcvg  34230  ofcc  34250  mbfmcst  34403  sibf0  34478  0rrv  34595  ccatmulgnn0dir  34686  plymul02  34690  plymulx  34692  txsconnlem  35422  cvmliftphtlem  35499  faclim  35928  matunitlindflem1  37937  poimirlem30  37971  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnclem  37992  iblmulc2nc  38006  itgmulc2nclem1  38007  itgmulc2nclem2  38008  itgmulc2nc  38009  itgabsnc  38010  ftc1cnnclem  38012  ftc1anclem3  38016  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc2nc  38023  repwsmet  38155  rrnequiv  38156  fsuppssindlem2  43025  fsuppssind  43026  mzpconstmpt  43172  mzpcompact2lem  43183  mendlmod  43617  mendassa  43618  mnringmulrcld  44655  expgrowthi  44760  expgrowth  44762  binomcxplemrat  44777  binomcxplemnotnn0  44783  climconstmpt  46086  iblconstmpt  46384  iblempty  46393  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stoweidlem21  46449  hoicvr  46976  nthrucw  47314  cjnpoly  47331  lindsrng01  48938  eufsn  49311  diag1a  49774  aacllem  50270  amgmlemALT  50272