MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fconstmpt Structured version   Visualization version   GIF version

Theorem fconstmpt 5074
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.
StepHypRef Expression
1 velsn 4140 . . . 4 (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
21anbi2i 725 . . 3 ((𝑥𝐴𝑦 ∈ {𝐵}) ↔ (𝑥𝐴𝑦 = 𝐵))
32opabbii 4643 . 2 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
4 df-xp 5033 . 2 (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})}
5 df-mpt 4639 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
63, 4, 53eqtr4i 2641 1 (𝐴 × {𝐵}) = (𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wcel 1976  {csn 4124  {copab 4636  cmpt 4637   × cxp 5025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-sn 4125  df-opab 4638  df-mpt 4639  df-xp 5033
This theorem is referenced by:  fconst  5988  fcoconst  6291  fmptsn  6315  fconstmpt2  6630  ofc12  6797  caofinvl  6799  xpexgALT  7029  cantnf  8450  cnfcom2lem  8458  repsconst  13318  harmonic  14378  geomulcvg  14394  vdwlem8  15478  ramcl  15519  pwsvscafval  15925  setcepi  16509  diag2  16656  pws0g  17097  0frgp  17963  pwsgsum  18149  lmhmvsca  18814  rrgsupp  19060  psrlinv  19166  psrlidm  19172  psrridm  19173  psrass23l  19177  psrass23  19179  mplcoe1  19234  mplcoe3  19235  mplcoe5  19237  mplmon2  19262  evlslem2  19281  evlslem1  19284  coe1z  19402  coe1mul2lem1  19406  coe1tm  19412  coe1sclmul  19421  coe1sclmul2  19423  evls1sca  19457  evl1sca  19467  uvcresum  19898  grpvrinv  19968  mdetunilem9  20192  pttoponconst  21157  cnmptc  21222  cnmptkc  21239  pt1hmeo  21366  tmdgsum2  21657  tsms0  21702  tgptsmscls  21710  resspwsds  21934  imasdsf1olem  21935  nmoeq0  22297  idnghm  22304  rrxcph  22932  ovolctb  23009  ovoliunnul  23026  vitalilem4  23130  vitalilem5  23131  ismbf  23147  mbfconst  23152  mbfss  23163  mbfmulc2re  23165  mbfneg  23167  mbfmulc2  23180  itg11  23208  itg2const  23257  itg2mulclem  23263  itg2mulc  23264  itg2monolem1  23267  itg0  23296  itgz  23297  itgvallem3  23302  iblposlem  23308  i1fibl  23324  itgitg1  23325  itgge0  23327  iblconst  23334  itgconst  23335  itgfsum  23343  iblmulc2  23347  itgmulc2lem1  23348  bddmulibl  23355  dvcmulf  23458  dvexp  23466  dvexp2  23467  dvmptid  23470  dvmptc  23471  dvef  23491  rolle  23501  dv11cn  23512  ftc1lem4  23550  ftc2  23555  tdeglem4  23568  ply1nzb  23630  plyconst  23710  plyeq0lem  23714  plypf1  23716  coeeulem  23728  plyco  23745  0dgr  23749  0dgrb  23750  dgrcolem2  23778  dgrco  23779  plyremlem  23807  elqaalem3  23824  iaa  23828  taylply2  23870  itgulm  23910  amgmlem  24460  lgam1  24534  ftalem7  24549  basellem8  24558  dchrfi  24724  dchrptlem3  24735  bra0  27986  padct  28678  xrge0mulc1cn  29108  esumnul  29230  esum0  29231  esumcvg  29268  ofcc  29288  mbfmcst  29441  sibf0  29516  0rrv  29633  ccatmulgnn0dir  29738  plymul02  29742  plymulx  29744  txsconlem  30269  cvmliftphtlem  30346  faclim  30678  matunitlindflem1  32358  poimirlem30  32392  ovoliunnfl  32404  voliunnfl  32406  volsupnfl  32407  itg2addnclem  32414  iblmulc2nc  32428  itgmulc2nclem1  32429  itgmulc2nclem2  32430  itgmulc2nc  32431  itgabsnc  32432  bddiblnc  32433  ftc1cnnclem  32436  ftc1anclem3  32440  ftc1anclem5  32442  ftc1anclem7  32444  ftc1anclem8  32445  ftc2nc  32447  repwsmet  32586  rrnequiv  32587  mzpconstmpt  36104  mzpcompact2lem  36115  mendlmod  36565  mendassa  36566  expgrowthi  37337  expgrowth  37339  binomcxplemrat  37354  binomcxplemnotnn0  37360  rnmptc  38131  climconstmpt  38508  iblconstmpt  38630  iblempty  38640  itgiccshift  38655  itgperiod  38656  itgsbtaddcnst  38657  stoweidlem21  38697  lindsrng01  42032  aacllem  42298  amgmlemALT  42300
  Copyright terms: Public domain W3C validator