Theorem fconstmpt 5712

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.

Step	Hyp	Ref	Expression
1		velsn 4599	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 635	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5171	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5656	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5186	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2793	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {csn 4583  {copab 5166   ↦ cmpt 5185   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sn 4584  df-opab 5167  df-mpt 5186  df-xp 5656

This theorem is used by:  fconst  6768  fcoconst  7135  fmptsn  7172  rnmptc  7213  fconstmpo  7537  ofc12  7723  caofinvl  7725  caofidlcan  7731  xpexgALT  7993  cantnf  9694  cnfcom2lem  9702  repsconst  14923  harmonic  16028  geomulcvg  16045  vdwlem8  17166  ramcl  17207  pwsvscafval  17666  setcepi  18263  diag2  18419  pws0g  18967  smndex1gbas  19098  smndex1gid  19100  smndex1igid  19102  smndex1igidOLD  19103  0frgp  19993  pwsgsum  20196  rrgsupp  20953  lmhmvsca  21320  uvcresum  22099  psrlinv  22263  psrlidm  22269  psrridm  22270  psrass23l  22274  psrass23  22276  mplcoe1  22346  mplcoe3  22347  mplcoe5  22349  mplmon2  22370  evlslem2  22388  evlslem1  22391  evlsvvval  22402  mhpsclcl  22468  psdmul  22487  psdmvr  22490  coe1z  22582  coe1mul2lem1  22586  coe1tm  22592  coe1sclmul  22601  coe1sclmul2  22603  evls1sca  22641  evl1sca  22652  evls1fpws  22687  grpvrinv  22714  mdetunilem9  22935  matunitlindflem1  22994  pttoponconst  23916  cnmptc  23981  cnmptkc  23998  pt1hmeo  24125  tmdgsum2  24415  tsms0  24461  tgptsmscls  24469  resspwsds  24691  imasdsf1olem  24692  nmoeq0  25055  idnghm  25062  rrxcph  25713  ovolctb  25811  ovoliunnul  25828  vitalilem4  25932  vitalilem5  25933  ismbf  25949  mbfconst  25954  mbfss  25967  mbfmulc2re  25969  mbfneg  25971  mbfmulc2  25984  itg11  26012  itg2const  26061  itg2mulclem  26067  itg2mulc  26068  itg2monolem1  26071  itg0  26100  itgz  26101  itgvallem3  26106  iblposlem  26112  i1fibl  26128  itgitg1  26129  itgge0  26131  iblconst  26138  itgconst  26139  itgfsum  26147  iblmulc2  26151  itgmulc2lem1  26152  bddmulibl  26159  bddiblnc  26162  dvcmulf  26265  dvexp  26273  dvexp2  26274  dvmptid  26277  dvmptc  26278  dvef  26300  rolle  26310  dv11cn  26321  ftc1lem4  26359  ftc2  26364  tdeglem4  26378  ply1nzb  26441  plyconst  26524  plyeq0lem  26529  plypf1  26531  coeeulem  26543  plyco  26560  0dgr  26564  0dgrb  26565  dgrcolem2  26593  dgrco  26594  plymul02  26601  plymulidp  26603  plyremlem  26625  elqaalem3  26644  iaaOLD  26652  taylply2  26695  itgulm  26735  amgmlem  27317  lgam1  27391  ftalem7  27406  basellem8  27415  dchrfi  27582  dchrptlem3  27593  istrkg2ld  28922  bra0  32552  padct  33352  cshw1s2  33563  gsumind  33948  mplasclco  34190  selvply1rhmlem2  34195  selvply1rhm0  34200  extvfvcl  34210  mplvrpmmhm  34220  psrgsum  34222  psrmonprod  34226  esplyfval3  34246  fedgmullem2  34304  extdgfialglem2  34367  zar0ring  34552  xrge0mulc1cn  34615  esumnul  34722  esum0  34723  esumcvg  34760  ofcc  34780  mbfmcst  34933  sibf0  35008  0rrv  35125  ccatmulgnn0dir  35216  txsconnlem  36047  cvmliftphtlem  36124  faclim  36553  poimirlem30  38611  ovoliunnfl  38623  voliunnfl  38625  volsupnfl  38626  itg2addnclem  38632  iblmulc2nc  38646  itgmulc2nclem1  38647  itgmulc2nclem2  38648  itgmulc2nc  38649  itgabsnc  38650  ftc1cnnclem  38652  ftc1anclem3  38656  ftc1anclem5  38658  ftc1anclem7  38660  ftc1anclem8  38661  ftc2nc  38663  repwsmet  38811  rrnequiv  38812  fsuppssindlem2  43663  fsuppssind  43664  mzpconstmpt  43794  mzpcompact2lem  43805  mendlmod  44234  mendassa  44235  mnringmulrcld  45269  expgrowthi  45360  expgrowth  45362  binomcxplemrat  45377  binomcxplemnotnn0  45383  climconstmpt  46711  iblconstmpt  47009  iblempty  47018  itgiccshift  47033  itgperiod  47034  itgsbtaddcnst  47035  stoweidlem21  47074  hoicvr  47601  cjnpoly  47982  lindsrng01  49623  eufsn  49995  diag1a  50456  aacllem  50982  veroquadmodzerod  51027  amgmlemALT  51031