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

Theorem fconstmpt 5085
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 4141 . . . 4 (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
21anbi2i 726 . . 3 ((𝑥𝐴𝑦 ∈ {𝐵}) ↔ (𝑥𝐴𝑦 = 𝐵))
32opabbii 4649 . 2 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
4 df-xp 5044 . 2 (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})}
5 df-mpt 4645 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
63, 4, 53eqtr4i 2642 1 (𝐴 × {𝐵}) = (𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1475  wcel 1977  {csn 4125  {copab 4642  cmpt 4643   × cxp 5036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-sn 4126  df-opab 4644  df-mpt 4645  df-xp 5044
This theorem is referenced by:  fconst  6004  fcoconst  6307  fmptsn  6338  fconstmpt2  6653  ofc12  6820  caofinvl  6822  xpexgALT  7052  cantnf  8473  cnfcom2lem  8481  repsconst  13370  harmonic  14430  geomulcvg  14446  vdwlem8  15530  ramcl  15571  pwsvscafval  15977  setcepi  16561  diag2  16708  pws0g  17149  0frgp  18015  pwsgsum  18201  lmhmvsca  18866  rrgsupp  19112  psrlinv  19218  psrlidm  19224  psrridm  19225  psrass23l  19229  psrass23  19231  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  mplmon2  19314  evlslem2  19333  evlslem1  19336  coe1z  19454  coe1mul2lem1  19458  coe1tm  19464  coe1sclmul  19473  coe1sclmul2  19475  evls1sca  19509  evl1sca  19519  uvcresum  19951  grpvrinv  20021  mdetunilem9  20245  pttoponconst  21210  cnmptc  21275  cnmptkc  21292  pt1hmeo  21419  tmdgsum2  21710  tsms0  21755  tgptsmscls  21763  resspwsds  21987  imasdsf1olem  21988  nmoeq0  22350  idnghm  22357  rrxcph  22988  ovolctb  23065  ovoliunnul  23082  vitalilem4  23186  vitalilem5  23187  ismbf  23203  mbfconst  23208  mbfss  23219  mbfmulc2re  23221  mbfneg  23223  mbfmulc2  23236  itg11  23264  itg2const  23313  itg2mulclem  23319  itg2mulc  23320  itg2monolem1  23323  itg0  23352  itgz  23353  itgvallem3  23358  iblposlem  23364  i1fibl  23380  itgitg1  23381  itgge0  23383  iblconst  23390  itgconst  23391  itgfsum  23399  iblmulc2  23403  itgmulc2lem1  23404  bddmulibl  23411  dvcmulf  23514  dvexp  23522  dvexp2  23523  dvmptid  23526  dvmptc  23527  dvef  23547  rolle  23557  dv11cn  23568  ftc1lem4  23606  ftc2  23611  tdeglem4  23624  ply1nzb  23686  plyconst  23766  plyeq0lem  23770  plypf1  23772  coeeulem  23784  plyco  23801  0dgr  23805  0dgrb  23806  dgrcolem2  23834  dgrco  23835  plyremlem  23863  elqaalem3  23880  iaa  23884  taylply2  23926  itgulm  23966  amgmlem  24516  lgam1  24590  ftalem7  24605  basellem8  24614  dchrfi  24780  dchrptlem3  24791  bra0  28193  padct  28885  xrge0mulc1cn  29315  esumnul  29437  esum0  29438  esumcvg  29475  ofcc  29495  mbfmcst  29648  sibf0  29723  0rrv  29840  ccatmulgnn0dir  29945  plymul02  29949  plymulx  29951  txsconlem  30476  cvmliftphtlem  30553  faclim  30885  matunitlindflem1  32575  poimirlem30  32609  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnclem  32631  iblmulc2nc  32645  itgmulc2nclem1  32646  itgmulc2nclem2  32647  itgmulc2nc  32648  itgabsnc  32649  bddiblnc  32650  ftc1cnnclem  32653  ftc1anclem3  32657  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anclem8  32662  ftc2nc  32664  repwsmet  32803  rrnequiv  32804  mzpconstmpt  36321  mzpcompact2lem  36332  mendlmod  36782  mendassa  36783  expgrowthi  37554  expgrowth  37556  binomcxplemrat  37571  binomcxplemnotnn0  37577  rnmptc  38348  climconstmpt  38725  iblconstmpt  38847  iblempty  38857  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stoweidlem21  38914  lindsrng01  42051  aacllem  42356  amgmlemALT  42358
  Copyright terms: Public domain W3C validator