Theorem fconstmpt 5702

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4591  {copab 5171   ↦ cmpt 5190   × cxp 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-sn 4592  df-opab 5172  df-mpt 5191  df-xp 5646

This theorem is referenced by:  fconst  6748  fcoconst  7108  fmptsn  7143  rnmptc  7183  fconstmpo  7508  ofc12  7685  caofinvl  7687  caofidlcan  7693  xpexgALT  7962  cantnf  9652  cnfcom2lem  9660  repsconst  14743  harmonic  15831  geomulcvg  15848  vdwlem8  16965  ramcl  17006  pwsvscafval  17463  setcepi  18056  diag2  18212  pws0g  18706  smndex1igid  18837  0frgp  19715  pwsgsum  19918  rrgsupp  20616  lmhmvsca  20958  uvcresum  21708  psrlinv  21870  psrlidm  21877  psrridm  21878  psrass23l  21882  psrass23  21884  mplcoe1  21950  mplcoe3  21951  mplcoe5  21953  mplmon2  21974  evlslem2  21992  evlslem1  21995  mhpsclcl  22040  psdmul  22059  psdmvr  22062  coe1z  22155  coe1mul2lem1  22159  coe1tm  22165  coe1sclmul  22174  coe1sclmul2  22176  evls1sca  22216  evl1sca  22227  evls1fpws  22262  grpvrinv  22292  mdetunilem9  22513  pttoponconst  23490  cnmptc  23555  cnmptkc  23572  pt1hmeo  23699  tmdgsum2  23989  tsms0  24035  tgptsmscls  24043  resspwsds  24266  imasdsf1olem  24267  nmoeq0  24630  idnghm  24637  rrxcph  25298  ovolctb  25397  ovoliunnul  25414  vitalilem4  25518  vitalilem5  25519  ismbf  25535  mbfconst  25540  mbfss  25553  mbfmulc2re  25555  mbfneg  25557  mbfmulc2  25570  itg11  25598  itg2const  25647  itg2mulclem  25653  itg2mulc  25654  itg2monolem1  25657  itg0  25687  itgz  25688  itgvallem3  25693  iblposlem  25699  i1fibl  25715  itgitg1  25716  itgge0  25718  iblconst  25725  itgconst  25726  itgfsum  25734  iblmulc2  25738  itgmulc2lem1  25739  bddmulibl  25746  bddiblnc  25749  dvcmulf  25854  dvexp  25863  dvexp2  25864  dvmptid  25867  dvmptc  25868  dvef  25890  rolle  25900  dv11cn  25912  ftc1lem4  25952  ftc2  25957  tdeglem4  25971  ply1nzb  26034  plyconst  26117  plyeq0lem  26121  plypf1  26123  coeeulem  26135  plyco  26152  0dgr  26156  0dgrb  26157  dgrcolem2  26186  dgrco  26187  plyremlem  26218  elqaalem3  26235  iaa  26239  taylply2  26281  taylply2OLD  26282  itgulm  26323  amgmlem  26906  lgam1  26980  ftalem7  26995  basellem8  27004  dchrfi  27172  dchrptlem3  27183  bra0  31885  padct  32649  cshw1s2  32888  fedgmullem2  33632  zar0ring  33874  xrge0mulc1cn  33937  esumnul  34044  esum0  34045  esumcvg  34082  ofcc  34102  mbfmcst  34256  sibf0  34331  0rrv  34448  ccatmulgnn0dir  34539  plymul02  34543  plymulx  34545  txsconnlem  35227  cvmliftphtlem  35304  faclim  35728  matunitlindflem1  37605  poimirlem30  37639  ovoliunnfl  37651  voliunnfl  37653  volsupnfl  37654  itg2addnclem  37660  iblmulc2nc  37674  itgmulc2nclem1  37675  itgmulc2nclem2  37676  itgmulc2nc  37677  itgabsnc  37678  ftc1cnnclem  37680  ftc1anclem3  37684  ftc1anclem5  37686  ftc1anclem7  37688  ftc1anclem8  37689  ftc2nc  37691  repwsmet  37823  rrnequiv  37824  evlsvvval  42544  fsuppssindlem2  42573  fsuppssind  42574  mzpconstmpt  42721  mzpcompact2lem  42732  mendlmod  43171  mendassa  43172  mnringmulrcld  44210  expgrowthi  44315  expgrowth  44317  binomcxplemrat  44332  binomcxplemnotnn0  44338  climconstmpt  45649  iblconstmpt  45947  iblempty  45956  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  stoweidlem21  46012  lindsrng01  48447  eufsn  48820  diag1a  49284  aacllem  49780  amgmlemALT  49782