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

Theorem fconstmpt 5608
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 4575 . . . 4 (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
21anbi2i 622 . . 3 ((𝑥𝐴𝑦 ∈ {𝐵}) ↔ (𝑥𝐴𝑦 = 𝐵))
32opabbii 5125 . 2 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
4 df-xp 5555 . 2 (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})}
5 df-mpt 5139 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
63, 4, 53eqtr4i 2854 1 (𝐴 × {𝐵}) = (𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1528  wcel 2105  {csn 4559  {copab 5120  cmpt 5138   × cxp 5547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-sn 4560  df-opab 5121  df-mpt 5139  df-xp 5555
This theorem is referenced by:  fconst  6559  fcoconst  6889  fmptsn  6922  rnmptc  6962  fconstmpo  7258  ofc12  7423  caofinvl  7425  xpexgALT  7673  cantnf  9145  cnfcom2lem  9153  repsconst  14124  harmonic  15204  geomulcvg  15222  vdwlem8  16314  ramcl  16355  pwsvscafval  16757  setcepi  17338  diag2  17485  pws0g  17937  0frgp  18836  pwsgsum  19033  lmhmvsca  19748  rrgsupp  19994  psrlinv  20107  psrlidm  20113  psrridm  20114  psrass23l  20118  psrass23  20120  mplcoe1  20176  mplcoe3  20177  mplcoe5  20179  mplmon2  20203  evlslem2  20222  evlslem1  20225  coe1z  20361  coe1mul2lem1  20365  coe1tm  20371  coe1sclmul  20380  coe1sclmul2  20382  evls1sca  20416  evl1sca  20427  uvcresum  20867  grpvrinv  20937  mdetunilem9  21159  pttoponconst  22135  cnmptc  22200  cnmptkc  22217  pt1hmeo  22344  tmdgsum2  22634  tsms0  22679  tgptsmscls  22687  resspwsds  22911  imasdsf1olem  22912  nmoeq0  23274  idnghm  23281  rrxcph  23924  ovolctb  24020  ovoliunnul  24037  vitalilem4  24141  vitalilem5  24142  ismbf  24158  mbfconst  24163  mbfss  24176  mbfmulc2re  24178  mbfneg  24180  mbfmulc2  24193  itg11  24221  itg2const  24270  itg2mulclem  24276  itg2mulc  24277  itg2monolem1  24280  itg0  24309  itgz  24310  itgvallem3  24315  iblposlem  24321  i1fibl  24337  itgitg1  24338  itgge0  24340  iblconst  24347  itgconst  24348  itgfsum  24356  iblmulc2  24360  itgmulc2lem1  24361  bddmulibl  24368  dvcmulf  24471  dvexp  24479  dvexp2  24480  dvmptid  24483  dvmptc  24484  dvef  24506  rolle  24516  dv11cn  24527  ftc1lem4  24565  ftc2  24570  tdeglem4  24583  ply1nzb  24645  plyconst  24725  plyeq0lem  24729  plypf1  24731  coeeulem  24743  plyco  24760  0dgr  24764  0dgrb  24765  dgrcolem2  24793  dgrco  24794  plyremlem  24822  elqaalem3  24839  iaa  24843  taylply2  24885  itgulm  24925  amgmlem  25495  lgam1  25569  ftalem7  25584  basellem8  25593  dchrfi  25759  dchrptlem3  25770  bra0  29655  padct  30382  cshw1s2  30562  fedgmullem2  30926  xrge0mulc1cn  31084  esumnul  31207  esum0  31208  esumcvg  31245  ofcc  31265  mbfmcst  31417  sibf0  31492  0rrv  31609  ccatmulgnn0dir  31712  plymul02  31716  plymulx  31718  txsconnlem  32385  cvmliftphtlem  32462  faclim  32876  matunitlindflem1  34770  poimirlem30  34804  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  itg2addnclem  34825  iblmulc2nc  34839  itgmulc2nclem1  34840  itgmulc2nclem2  34841  itgmulc2nc  34842  itgabsnc  34843  bddiblnc  34844  ftc1cnnclem  34847  ftc1anclem3  34851  ftc1anclem5  34853  ftc1anclem7  34855  ftc1anclem8  34856  ftc2nc  34858  repwsmet  34995  rrnequiv  34996  mzpconstmpt  39217  mzpcompact2lem  39228  mendlmod  39673  mendassa  39674  expgrowthi  40545  expgrowth  40547  binomcxplemrat  40562  binomcxplemnotnn0  40568  climconstmpt  41819  iblconstmpt  42121  iblempty  42130  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  stoweidlem21  42187  smndex1igid  43974  lindsrng01  44421  aacllem  44800  amgmlemALT  44802
  Copyright terms: Public domain W3C validator