Theorem fconstmpt 5750

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

Syntax hints:   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {csn 4630  {copab 5209   ↦ cmpt 5230   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-sn 4631  df-opab 5210  df-mpt 5231  df-xp 5694

This theorem is referenced by:  fconst  6794  fcoconst  7153  fmptsn  7186  rnmptc  7226  fconstmpo  7549  ofc12  7726  caofinvl  7728  xpexgALT  8004  cantnf  9730  cnfcom2lem  9738  repsconst  14806  harmonic  15891  geomulcvg  15908  vdwlem8  17021  ramcl  17062  pwsvscafval  17540  setcepi  18141  diag2  18301  pws0g  18798  smndex1igid  18929  0frgp  19811  pwsgsum  20014  rrgsupp  20717  lmhmvsca  21061  uvcresum  21830  psrlinv  21992  psrlidm  21999  psrridm  22000  psrass23l  22004  psrass23  22006  mplcoe1  22072  mplcoe3  22073  mplcoe5  22075  mplmon2  22102  evlslem2  22120  evlslem1  22123  mhpsclcl  22168  psdmul  22187  coe1z  22281  coe1mul2lem1  22285  coe1tm  22291  coe1sclmul  22300  coe1sclmul2  22302  evls1sca  22342  evl1sca  22353  evls1fpws  22388  grpvrinv  22418  mdetunilem9  22641  pttoponconst  23620  cnmptc  23685  cnmptkc  23702  pt1hmeo  23829  tmdgsum2  24119  tsms0  24165  tgptsmscls  24173  resspwsds  24397  imasdsf1olem  24398  nmoeq0  24772  idnghm  24779  rrxcph  25439  ovolctb  25538  ovoliunnul  25555  vitalilem4  25659  vitalilem5  25660  ismbf  25676  mbfconst  25681  mbfss  25694  mbfmulc2re  25696  mbfneg  25698  mbfmulc2  25711  itg11  25739  itg2const  25789  itg2mulclem  25795  itg2mulc  25796  itg2monolem1  25799  itg0  25829  itgz  25830  itgvallem3  25835  iblposlem  25841  i1fibl  25857  itgitg1  25858  itgge0  25860  iblconst  25867  itgconst  25868  itgfsum  25876  iblmulc2  25880  itgmulc2lem1  25881  bddmulibl  25888  bddiblnc  25891  dvcmulf  25996  dvexp  26005  dvexp2  26006  dvmptid  26009  dvmptc  26010  dvef  26032  rolle  26042  dv11cn  26054  ftc1lem4  26094  ftc2  26099  tdeglem4  26113  ply1nzb  26176  plyconst  26259  plyeq0lem  26263  plypf1  26265  coeeulem  26277  plyco  26294  0dgr  26298  0dgrb  26299  dgrcolem2  26328  dgrco  26329  plyremlem  26360  elqaalem3  26377  iaa  26381  taylply2  26423  taylply2OLD  26424  itgulm  26465  amgmlem  27047  lgam1  27121  ftalem7  27136  basellem8  27145  dchrfi  27313  dchrptlem3  27324  bra0  31978  padct  32736  cshw1s2  32929  fedgmullem2  33657  zar0ring  33838  xrge0mulc1cn  33901  esumnul  34028  esum0  34029  esumcvg  34066  ofcc  34086  mbfmcst  34240  sibf0  34315  0rrv  34432  ccatmulgnn0dir  34535  plymul02  34539  plymulx  34541  txsconnlem  35224  cvmliftphtlem  35301  faclim  35725  matunitlindflem1  37602  poimirlem30  37636  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  itg2addnclem  37657  iblmulc2nc  37671  itgmulc2nclem1  37672  itgmulc2nclem2  37673  itgmulc2nc  37674  itgabsnc  37675  ftc1cnnclem  37677  ftc1anclem3  37681  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  ftc2nc  37688  repwsmet  37820  rrnequiv  37821  evlsvvval  42549  fsuppssindlem2  42578  fsuppssind  42579  mzpconstmpt  42727  mzpcompact2lem  42738  mendlmod  43177  mendassa  43178  mnringmulrcld  44223  expgrowthi  44328  expgrowth  44330  binomcxplemrat  44345  binomcxplemnotnn0  44351  climconstmpt  45613  iblconstmpt  45911  iblempty  45920  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stoweidlem21  45976  lindsrng01  48313  eufsn  48671  aacllem  49031  amgmlemALT  49033