Theorem fconstmpt 5503

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 4490	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 622	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5031	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5452	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5044	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2828	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 396   = wceq 1522   ∈ wcel 2080  {csn 4474  {copab 5026   ↦ cmpt 5043   × cxp 5444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-v 3438  df-sn 4475  df-opab 5027  df-mpt 5044  df-xp 5452

This theorem is referenced by:  fconst  6436  fcoconst  6762  fmptsn  6795  rnmptc  6839  fconstmpo  7128  ofc12  7295  caofinvl  7297  xpexgALT  7541  cantnf  9005  cnfcom2lem  9013  repsconst  13970  harmonic  15047  geomulcvg  15065  vdwlem8  16153  ramcl  16194  pwsvscafval  16596  setcepi  17177  diag2  17324  pws0g  17765  0frgp  18632  pwsgsum  18819  lmhmvsca  19507  rrgsupp  19753  psrlinv  19865  psrlidm  19871  psrridm  19872  psrass23l  19876  psrass23  19878  mplcoe1  19933  mplcoe3  19934  mplcoe5  19936  mplmon2  19960  evlslem2  19979  evlslem1  19982  coe1z  20114  coe1mul2lem1  20118  coe1tm  20124  coe1sclmul  20133  coe1sclmul2  20135  evls1sca  20169  evl1sca  20179  uvcresum  20619  grpvrinv  20689  mdetunilem9  20913  pttoponconst  21889  cnmptc  21954  cnmptkc  21971  pt1hmeo  22098  tmdgsum2  22388  tsms0  22433  tgptsmscls  22441  resspwsds  22665  imasdsf1olem  22666  nmoeq0  23028  idnghm  23035  rrxcph  23678  ovolctb  23774  ovoliunnul  23791  vitalilem4  23895  vitalilem5  23896  ismbf  23912  mbfconst  23917  mbfss  23930  mbfmulc2re  23932  mbfneg  23934  mbfmulc2  23947  itg11  23975  itg2const  24024  itg2mulclem  24030  itg2mulc  24031  itg2monolem1  24034  itg0  24063  itgz  24064  itgvallem3  24069  iblposlem  24075  i1fibl  24091  itgitg1  24092  itgge0  24094  iblconst  24101  itgconst  24102  itgfsum  24110  iblmulc2  24114  itgmulc2lem1  24115  bddmulibl  24122  dvcmulf  24225  dvexp  24233  dvexp2  24234  dvmptid  24237  dvmptc  24238  dvef  24260  rolle  24270  dv11cn  24281  ftc1lem4  24319  ftc2  24324  tdeglem4  24337  ply1nzb  24399  plyconst  24479  plyeq0lem  24483  plypf1  24485  coeeulem  24497  plyco  24514  0dgr  24518  0dgrb  24519  dgrcolem2  24547  dgrco  24548  plyremlem  24576  elqaalem3  24593  iaa  24597  taylply2  24639  itgulm  24679  amgmlem  25249  lgam1  25323  ftalem7  25338  basellem8  25347  dchrfi  25513  dchrptlem3  25524  bra0  29410  padct  30135  cshw1s2  30300  fedgmullem2  30622  xrge0mulc1cn  30793  esumnul  30916  esum0  30917  esumcvg  30954  ofcc  30974  mbfmcst  31126  sibf0  31201  0rrv  31318  ccatmulgnn0dir  31421  plymul02  31425  plymulx  31427  txsconnlem  32089  cvmliftphtlem  32166  faclim  32580  matunitlindflem1  34432  poimirlem30  34466  ovoliunnfl  34478  voliunnfl  34480  volsupnfl  34481  itg2addnclem  34487  iblmulc2nc  34501  itgmulc2nclem1  34502  itgmulc2nclem2  34503  itgmulc2nc  34504  itgabsnc  34505  bddiblnc  34506  ftc1cnnclem  34509  ftc1anclem3  34513  ftc1anclem5  34515  ftc1anclem7  34517  ftc1anclem8  34518  ftc2nc  34520  repwsmet  34657  rrnequiv  34658  mzpconstmpt  38835  mzpcompact2lem  38846  mendlmod  39291  mendassa  39292  expgrowthi  40216  expgrowth  40218  binomcxplemrat  40233  binomcxplemnotnn0  40239  climconstmpt  41494  iblconstmpt  41796  iblempty  41805  itgiccshift  41820  itgperiod  41821  itgsbtaddcnst  41822  stoweidlem21  41862  lindsrng01  44017  aacllem  44396  amgmlemALT  44398