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

Theorem fconstmpt 5582
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 4544 . . . 4 (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
21anbi2i 625 . . 3 ((𝑥𝐴𝑦 ∈ {𝐵}) ↔ (𝑥𝐴𝑦 = 𝐵))
32opabbii 5100 . 2 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
4 df-xp 5529 . 2 (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})}
5 df-mpt 5114 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
63, 4, 53eqtr4i 2834 1 (𝐴 × {𝐵}) = (𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1538  wcel 2112  {csn 4528  {copab 5095  cmpt 5113   × cxp 5521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-sn 4529  df-opab 5096  df-mpt 5114  df-xp 5529
This theorem is referenced by:  fconst  6543  fcoconst  6877  fmptsn  6910  rnmptc  6950  rnmptcOLD  6951  fconstmpo  7252  ofc12  7418  caofinvl  7420  xpexgALT  7668  cantnf  9144  cnfcom2lem  9152  repsconst  14129  harmonic  15210  geomulcvg  15228  vdwlem8  16318  ramcl  16359  pwsvscafval  16763  setcepi  17344  diag2  17491  pws0g  17943  smndex1igid  18065  0frgp  18901  pwsgsum  19099  lmhmvsca  19814  rrgsupp  20061  uvcresum  20486  psrlinv  20639  psrlidm  20645  psrridm  20646  psrass23l  20650  psrass23  20652  mplcoe1  20709  mplcoe3  20710  mplcoe5  20712  mplmon2  20736  evlslem2  20755  evlslem1  20758  coe1z  20896  coe1mul2lem1  20900  coe1tm  20906  coe1sclmul  20915  coe1sclmul2  20917  evls1sca  20951  evl1sca  20962  grpvrinv  21007  mdetunilem9  21229  pttoponconst  22206  cnmptc  22271  cnmptkc  22288  pt1hmeo  22415  tmdgsum2  22705  tsms0  22751  tgptsmscls  22759  resspwsds  22983  imasdsf1olem  22984  nmoeq0  23346  idnghm  23353  rrxcph  24000  ovolctb  24098  ovoliunnul  24115  vitalilem4  24219  vitalilem5  24220  ismbf  24236  mbfconst  24241  mbfss  24254  mbfmulc2re  24256  mbfneg  24258  mbfmulc2  24271  itg11  24299  itg2const  24348  itg2mulclem  24354  itg2mulc  24355  itg2monolem1  24358  itg0  24387  itgz  24388  itgvallem3  24393  iblposlem  24399  i1fibl  24415  itgitg1  24416  itgge0  24418  iblconst  24425  itgconst  24426  itgfsum  24434  iblmulc2  24438  itgmulc2lem1  24439  bddmulibl  24446  bddiblnc  24449  dvcmulf  24552  dvexp  24560  dvexp2  24561  dvmptid  24564  dvmptc  24565  dvef  24587  rolle  24597  dv11cn  24608  ftc1lem4  24646  ftc2  24651  tdeglem4  24665  ply1nzb  24727  plyconst  24807  plyeq0lem  24811  plypf1  24813  coeeulem  24825  plyco  24842  0dgr  24846  0dgrb  24847  dgrcolem2  24875  dgrco  24876  plyremlem  24904  elqaalem3  24921  iaa  24925  taylply2  24967  itgulm  25007  amgmlem  25579  lgam1  25653  ftalem7  25668  basellem8  25677  dchrfi  25843  dchrptlem3  25854  bra0  29737  padct  30485  cshw1s2  30664  fedgmullem2  31118  zar0ring  31235  xrge0mulc1cn  31298  esumnul  31421  esum0  31422  esumcvg  31459  ofcc  31479  mbfmcst  31631  sibf0  31706  0rrv  31823  ccatmulgnn0dir  31926  plymul02  31930  plymulx  31932  txsconnlem  32601  cvmliftphtlem  32678  faclim  33092  matunitlindflem1  35052  poimirlem30  35086  ovoliunnfl  35098  voliunnfl  35100  volsupnfl  35101  itg2addnclem  35107  iblmulc2nc  35121  itgmulc2nclem1  35122  itgmulc2nclem2  35123  itgmulc2nc  35124  itgabsnc  35125  ftc1cnnclem  35127  ftc1anclem3  35131  ftc1anclem5  35133  ftc1anclem7  35135  ftc1anclem8  35136  ftc2nc  35138  repwsmet  35271  rrnequiv  35272  fsuppssindlem2  39455  fsuppssind  39456  mzpconstmpt  39678  mzpcompact2lem  39689  mendlmod  40134  mendassa  40135  mnringmulrcld  40933  expgrowthi  41034  expgrowth  41036  binomcxplemrat  41051  binomcxplemnotnn0  41057  climconstmpt  42297  iblconstmpt  42595  iblempty  42604  itgiccshift  42619  itgperiod  42620  itgsbtaddcnst  42621  stoweidlem21  42660  lindsrng01  44874  aacllem  45326  amgmlemALT  45328
  Copyright terms: Public domain W3C validator