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

Theorem fconstmpt 5695
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 4603 . . . 4 (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
21anbi2i 624 . . 3 ((𝑥𝐴𝑦 ∈ {𝐵}) ↔ (𝑥𝐴𝑦 = 𝐵))
32opabbii 5173 . 2 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
4 df-xp 5640 . 2 (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})}
5 df-mpt 5190 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
63, 4, 53eqtr4i 2775 1 (𝐴 × {𝐵}) = (𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  wcel 2107  {csn 4587  {copab 5168  cmpt 5189   × cxp 5632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-sn 4588  df-opab 5169  df-mpt 5190  df-xp 5640
This theorem is referenced by:  fconst  6729  fcoconst  7081  fmptsn  7114  rnmptc  7157  rnmptcOLD  7158  fconstmpo  7474  ofc12  7646  caofinvl  7648  xpexgALT  7915  cantnf  9630  cnfcom2lem  9638  repsconst  14661  harmonic  15745  geomulcvg  15762  vdwlem8  16861  ramcl  16902  pwsvscafval  17377  setcepi  17975  diag2  18135  pws0g  18593  smndex1igid  18715  0frgp  19562  pwsgsum  19760  lmhmvsca  20509  rrgsupp  20764  uvcresum  21202  psrlinv  21368  psrlidm  21375  psrridm  21376  psrass23l  21380  psrass23  21382  mplcoe1  21441  mplcoe3  21442  mplcoe5  21444  mplmon2  21472  evlslem2  21492  evlslem1  21495  mhpsclcl  21540  coe1z  21637  coe1mul2lem1  21641  coe1tm  21647  coe1sclmul  21656  coe1sclmul2  21658  evls1sca  21692  evl1sca  21703  grpvrinv  21748  mdetunilem9  21972  pttoponconst  22951  cnmptc  23016  cnmptkc  23033  pt1hmeo  23160  tmdgsum2  23450  tsms0  23496  tgptsmscls  23504  resspwsds  23728  imasdsf1olem  23729  nmoeq0  24103  idnghm  24110  rrxcph  24759  ovolctb  24857  ovoliunnul  24874  vitalilem4  24978  vitalilem5  24979  ismbf  24995  mbfconst  25000  mbfss  25013  mbfmulc2re  25015  mbfneg  25017  mbfmulc2  25030  itg11  25058  itg2const  25108  itg2mulclem  25114  itg2mulc  25115  itg2monolem1  25118  itg0  25147  itgz  25148  itgvallem3  25153  iblposlem  25159  i1fibl  25175  itgitg1  25176  itgge0  25178  iblconst  25185  itgconst  25186  itgfsum  25194  iblmulc2  25198  itgmulc2lem1  25199  bddmulibl  25206  bddiblnc  25209  dvcmulf  25312  dvexp  25320  dvexp2  25321  dvmptid  25324  dvmptc  25325  dvef  25347  rolle  25357  dv11cn  25368  ftc1lem4  25406  ftc2  25411  tdeglem4  25427  tdeglem4OLD  25428  ply1nzb  25490  plyconst  25570  plyeq0lem  25574  plypf1  25576  coeeulem  25588  plyco  25605  0dgr  25609  0dgrb  25610  dgrcolem2  25638  dgrco  25639  plyremlem  25667  elqaalem3  25684  iaa  25688  taylply2  25730  itgulm  25770  amgmlem  26342  lgam1  26416  ftalem7  26431  basellem8  26440  dchrfi  26606  dchrptlem3  26617  bra0  30895  padct  31639  cshw1s2  31817  evls1fpws  32274  fedgmullem2  32328  zar0ring  32462  xrge0mulc1cn  32525  esumnul  32650  esum0  32651  esumcvg  32688  ofcc  32708  mbfmcst  32862  sibf0  32937  0rrv  33054  ccatmulgnn0dir  33157  plymul02  33161  plymulx  33163  txsconnlem  33837  cvmliftphtlem  33914  faclim  34322  matunitlindflem1  36077  poimirlem30  36111  ovoliunnfl  36123  voliunnfl  36125  volsupnfl  36126  itg2addnclem  36132  iblmulc2nc  36146  itgmulc2nclem1  36147  itgmulc2nclem2  36148  itgmulc2nc  36149  itgabsnc  36150  ftc1cnnclem  36152  ftc1anclem3  36156  ftc1anclem5  36158  ftc1anclem7  36160  ftc1anclem8  36161  ftc2nc  36163  repwsmet  36296  rrnequiv  36297  evlsbagval  40751  fsuppssindlem2  40770  fsuppssind  40771  mzpconstmpt  41066  mzpcompact2lem  41077  mendlmod  41523  mendassa  41524  mnringmulrcld  42515  expgrowthi  42620  expgrowth  42622  binomcxplemrat  42637  binomcxplemnotnn0  42643  climconstmpt  43906  iblconstmpt  44204  iblempty  44213  itgiccshift  44228  itgperiod  44229  itgsbtaddcnst  44230  stoweidlem21  44269  lindsrng01  46556  eufsn  46915  aacllem  47255  amgmlemALT  47257
  Copyright terms: Public domain W3C validator