Theorem fconstmpt 5737

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

Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {csn 4628  {copab 5210   ↦ cmpt 5231   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sn 4629  df-opab 5211  df-mpt 5232  df-xp 5682

This theorem is referenced by:  fconst  6775  fcoconst  7129  fmptsn  7162  rnmptc  7205  rnmptcOLD  7206  fconstmpo  7522  ofc12  7695  caofinvl  7697  xpexgALT  7965  cantnf  9685  cnfcom2lem  9693  repsconst  14719  harmonic  15802  geomulcvg  15819  vdwlem8  16918  ramcl  16959  pwsvscafval  17437  setcepi  18035  diag2  18195  pws0g  18658  smndex1igid  18782  0frgp  19642  pwsgsum  19845  lmhmvsca  20649  rrgsupp  20900  uvcresum  21340  psrlinv  21508  psrlidm  21515  psrridm  21516  psrass23l  21520  psrass23  21522  mplcoe1  21584  mplcoe3  21585  mplcoe5  21587  mplmon2  21614  evlslem2  21634  evlslem1  21637  mhpsclcl  21682  coe1z  21777  coe1mul2lem1  21781  coe1tm  21787  coe1sclmul  21796  coe1sclmul2  21798  evls1sca  21834  evl1sca  21845  grpvrinv  21890  mdetunilem9  22114  pttoponconst  23093  cnmptc  23158  cnmptkc  23175  pt1hmeo  23302  tmdgsum2  23592  tsms0  23638  tgptsmscls  23646  resspwsds  23870  imasdsf1olem  23871  nmoeq0  24245  idnghm  24252  rrxcph  24901  ovolctb  24999  ovoliunnul  25016  vitalilem4  25120  vitalilem5  25121  ismbf  25137  mbfconst  25142  mbfss  25155  mbfmulc2re  25157  mbfneg  25159  mbfmulc2  25172  itg11  25200  itg2const  25250  itg2mulclem  25256  itg2mulc  25257  itg2monolem1  25260  itg0  25289  itgz  25290  itgvallem3  25295  iblposlem  25301  i1fibl  25317  itgitg1  25318  itgge0  25320  iblconst  25327  itgconst  25328  itgfsum  25336  iblmulc2  25340  itgmulc2lem1  25341  bddmulibl  25348  bddiblnc  25351  dvcmulf  25454  dvexp  25462  dvexp2  25463  dvmptid  25466  dvmptc  25467  dvef  25489  rolle  25499  dv11cn  25510  ftc1lem4  25548  ftc2  25553  tdeglem4  25569  tdeglem4OLD  25570  ply1nzb  25632  plyconst  25712  plyeq0lem  25716  plypf1  25718  coeeulem  25730  plyco  25747  0dgr  25751  0dgrb  25752  dgrcolem2  25780  dgrco  25781  plyremlem  25809  elqaalem3  25826  iaa  25830  taylply2  25872  itgulm  25912  amgmlem  26484  lgam1  26558  ftalem7  26573  basellem8  26582  dchrfi  26748  dchrptlem3  26759  bra0  31191  padct  31932  cshw1s2  32112  evls1fpws  32635  fedgmullem2  32704  zar0ring  32847  xrge0mulc1cn  32910  esumnul  33035  esum0  33036  esumcvg  33073  ofcc  33093  mbfmcst  33247  sibf0  33322  0rrv  33439  ccatmulgnn0dir  33542  plymul02  33546  plymulx  33548  txsconnlem  34220  cvmliftphtlem  34297  faclim  34705  matunitlindflem1  36473  poimirlem30  36507  ovoliunnfl  36519  voliunnfl  36521  volsupnfl  36522  itg2addnclem  36528  iblmulc2nc  36542  itgmulc2nclem1  36543  itgmulc2nclem2  36544  itgmulc2nc  36545  itgabsnc  36546  ftc1cnnclem  36548  ftc1anclem3  36552  ftc1anclem5  36554  ftc1anclem7  36556  ftc1anclem8  36557  ftc2nc  36559  repwsmet  36691  rrnequiv  36692  evlsvvval  41133  fsuppssindlem2  41162  fsuppssind  41163  mzpconstmpt  41464  mzpcompact2lem  41475  mendlmod  41921  mendassa  41922  mnringmulrcld  42973  expgrowthi  43078  expgrowth  43080  binomcxplemrat  43095  binomcxplemnotnn0  43101  climconstmpt  44361  iblconstmpt  44659  iblempty  44668  itgiccshift  44683  itgperiod  44684  itgsbtaddcnst  44685  stoweidlem21  44724  lindsrng01  47103  eufsn  47462  aacllem  47802  amgmlemALT  47804