Theorem fconstmpt 5681

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {csn 4575  {copab 5155   ↦ cmpt 5174   × cxp 5617

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-sn 4576  df-opab 5156  df-mpt 5175  df-xp 5625

This theorem is referenced by:  fconst  6715  fcoconst  7073  fmptsn  7107  rnmptc  7147  fconstmpo  7469  ofc12  7646  caofinvl  7648  caofidlcan  7654  xpexgALT  7919  cantnf  9589  cnfcom2lem  9597  repsconst  14685  harmonic  15772  geomulcvg  15789  vdwlem8  16906  ramcl  16947  pwsvscafval  17404  setcepi  18001  diag2  18157  pws0g  18687  smndex1igid  18818  0frgp  19697  pwsgsum  19900  rrgsupp  20622  lmhmvsca  20985  uvcresum  21736  psrlinv  21898  psrlidm  21905  psrridm  21906  psrass23l  21910  psrass23  21912  mplcoe1  21978  mplcoe3  21979  mplcoe5  21981  mplmon2  22002  evlslem2  22020  evlslem1  22023  mhpsclcl  22068  psdmul  22087  psdmvr  22090  coe1z  22183  coe1mul2lem1  22187  coe1tm  22193  coe1sclmul  22202  coe1sclmul2  22204  evls1sca  22244  evl1sca  22255  evls1fpws  22290  grpvrinv  22320  mdetunilem9  22541  pttoponconst  23518  cnmptc  23583  cnmptkc  23600  pt1hmeo  23727  tmdgsum2  24017  tsms0  24063  tgptsmscls  24071  resspwsds  24293  imasdsf1olem  24294  nmoeq0  24657  idnghm  24664  rrxcph  25325  ovolctb  25424  ovoliunnul  25441  vitalilem4  25545  vitalilem5  25546  ismbf  25562  mbfconst  25567  mbfss  25580  mbfmulc2re  25582  mbfneg  25584  mbfmulc2  25597  itg11  25625  itg2const  25674  itg2mulclem  25680  itg2mulc  25681  itg2monolem1  25684  itg0  25714  itgz  25715  itgvallem3  25720  iblposlem  25726  i1fibl  25742  itgitg1  25743  itgge0  25745  iblconst  25752  itgconst  25753  itgfsum  25761  iblmulc2  25765  itgmulc2lem1  25766  bddmulibl  25773  bddiblnc  25776  dvcmulf  25881  dvexp  25890  dvexp2  25891  dvmptid  25894  dvmptc  25895  dvef  25917  rolle  25927  dv11cn  25939  ftc1lem4  25979  ftc2  25984  tdeglem4  25998  ply1nzb  26061  plyconst  26144  plyeq0lem  26148  plypf1  26150  coeeulem  26162  plyco  26179  0dgr  26183  0dgrb  26184  dgrcolem2  26213  dgrco  26214  plyremlem  26245  elqaalem3  26262  iaa  26266  taylply2  26308  taylply2OLD  26309  itgulm  26350  amgmlem  26933  lgam1  27007  ftalem7  27022  basellem8  27031  dchrfi  27199  dchrptlem3  27210  bra0  31937  padct  32708  cshw1s2  32948  gsumind  33317  mplvrpmmhm  33583  fedgmullem2  33650  extdgfialglem2  33713  zar0ring  33898  xrge0mulc1cn  33961  esumnul  34068  esum0  34069  esumcvg  34106  ofcc  34126  mbfmcst  34279  sibf0  34354  0rrv  34471  ccatmulgnn0dir  34562  plymul02  34566  plymulx  34568  txsconnlem  35291  cvmliftphtlem  35368  faclim  35797  matunitlindflem1  37662  poimirlem30  37696  ovoliunnfl  37708  voliunnfl  37710  volsupnfl  37711  itg2addnclem  37717  iblmulc2nc  37731  itgmulc2nclem1  37732  itgmulc2nclem2  37733  itgmulc2nc  37734  itgabsnc  37735  ftc1cnnclem  37737  ftc1anclem3  37741  ftc1anclem5  37743  ftc1anclem7  37745  ftc1anclem8  37746  ftc2nc  37748  repwsmet  37880  rrnequiv  37881  evlsvvval  42662  fsuppssindlem2  42691  fsuppssind  42692  mzpconstmpt  42838  mzpcompact2lem  42849  mendlmod  43287  mendassa  43288  mnringmulrcld  44326  expgrowthi  44431  expgrowth  44433  binomcxplemrat  44448  binomcxplemnotnn0  44454  climconstmpt  45761  iblconstmpt  46059  iblempty  46068  itgiccshift  46083  itgperiod  46084  itgsbtaddcnst  46085  stoweidlem21  46124  nthrucw  46989  cjnpoly  46994  lindsrng01  48574  eufsn  48947  diag1a  49411  aacllem  49907  amgmlemALT  49909