Theorem fconstmpt 5700

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4589  {copab 5169   ↦ cmpt 5188   × cxp 5636

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-sn 4590  df-opab 5170  df-mpt 5189  df-xp 5644

This theorem is referenced by:  fconst  6746  fcoconst  7106  fmptsn  7141  rnmptc  7181  fconstmpo  7506  ofc12  7683  caofinvl  7685  caofidlcan  7691  xpexgALT  7960  cantnf  9646  cnfcom2lem  9654  repsconst  14737  harmonic  15825  geomulcvg  15842  vdwlem8  16959  ramcl  17000  pwsvscafval  17457  setcepi  18050  diag2  18206  pws0g  18700  smndex1igid  18831  0frgp  19709  pwsgsum  19912  rrgsupp  20610  lmhmvsca  20952  uvcresum  21702  psrlinv  21864  psrlidm  21871  psrridm  21872  psrass23l  21876  psrass23  21878  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  mplmon2  21968  evlslem2  21986  evlslem1  21989  mhpsclcl  22034  psdmul  22053  psdmvr  22056  coe1z  22149  coe1mul2lem1  22153  coe1tm  22159  coe1sclmul  22168  coe1sclmul2  22170  evls1sca  22210  evl1sca  22221  evls1fpws  22256  grpvrinv  22286  mdetunilem9  22507  pttoponconst  23484  cnmptc  23549  cnmptkc  23566  pt1hmeo  23693  tmdgsum2  23983  tsms0  24029  tgptsmscls  24037  resspwsds  24260  imasdsf1olem  24261  nmoeq0  24624  idnghm  24631  rrxcph  25292  ovolctb  25391  ovoliunnul  25408  vitalilem4  25512  vitalilem5  25513  ismbf  25529  mbfconst  25534  mbfss  25547  mbfmulc2re  25549  mbfneg  25551  mbfmulc2  25564  itg11  25592  itg2const  25641  itg2mulclem  25647  itg2mulc  25648  itg2monolem1  25651  itg0  25681  itgz  25682  itgvallem3  25687  iblposlem  25693  i1fibl  25709  itgitg1  25710  itgge0  25712  iblconst  25719  itgconst  25720  itgfsum  25728  iblmulc2  25732  itgmulc2lem1  25733  bddmulibl  25740  bddiblnc  25743  dvcmulf  25848  dvexp  25857  dvexp2  25858  dvmptid  25861  dvmptc  25862  dvef  25884  rolle  25894  dv11cn  25906  ftc1lem4  25946  ftc2  25951  tdeglem4  25965  ply1nzb  26028  plyconst  26111  plyeq0lem  26115  plypf1  26117  coeeulem  26129  plyco  26146  0dgr  26150  0dgrb  26151  dgrcolem2  26180  dgrco  26181  plyremlem  26212  elqaalem3  26229  iaa  26233  taylply2  26275  taylply2OLD  26276  itgulm  26317  amgmlem  26900  lgam1  26974  ftalem7  26989  basellem8  26998  dchrfi  27166  dchrptlem3  27177  bra0  31879  padct  32643  cshw1s2  32882  fedgmullem2  33626  zar0ring  33868  xrge0mulc1cn  33931  esumnul  34038  esum0  34039  esumcvg  34076  ofcc  34096  mbfmcst  34250  sibf0  34325  0rrv  34442  ccatmulgnn0dir  34533  plymul02  34537  plymulx  34539  txsconnlem  35227  cvmliftphtlem  35304  faclim  35733  matunitlindflem1  37610  poimirlem30  37644  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnclem  37665  iblmulc2nc  37679  itgmulc2nclem1  37680  itgmulc2nclem2  37681  itgmulc2nc  37682  itgabsnc  37683  ftc1cnnclem  37685  ftc1anclem3  37689  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc2nc  37696  repwsmet  37828  rrnequiv  37829  evlsvvval  42551  fsuppssindlem2  42580  fsuppssind  42581  mzpconstmpt  42728  mzpcompact2lem  42739  mendlmod  43178  mendassa  43179  mnringmulrcld  44217  expgrowthi  44322  expgrowth  44324  binomcxplemrat  44339  binomcxplemnotnn0  44345  climconstmpt  45656  iblconstmpt  45954  iblempty  45963  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stoweidlem21  46019  cjnpoly  46890  lindsrng01  48457  eufsn  48830  diag1a  49294  aacllem  49790  amgmlemALT  49792