Theorem fconstmpt 5709

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 5653	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5186	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2793	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sn 4584  df-opab 5167  df-mpt 5186  df-xp 5653

This theorem is used by:  fconst  6756  fcoconst  7123  fmptsn  7160  rnmptc  7201  fconstmpo  7525  ofc12  7706  caofinvl  7708  caofidlcan  7714  xpexgALT  7976  cantnf  9672  cnfcom2lem  9680  repsconst  14890  harmonic  15995  geomulcvg  16012  vdwlem8  17127  ramcl  17168  pwsvscafval  17627  setcepi  18224  diag2  18380  pws0g  18928  smndex1gbas  19059  smndex1gid  19061  smndex1igid  19063  smndex1igidOLD  19064  0frgp  19954  pwsgsum  20157  rrgsupp  20914  lmhmvsca  21281  uvcresum  22060  psrlinv  22224  psrlidm  22230  psrridm  22231  psrass23l  22235  psrass23  22237  mplcoe1  22307  mplcoe3  22308  mplcoe5  22310  mplmon2  22331  evlslem2  22349  evlslem1  22352  evlsvvval  22363  mhpsclcl  22429  psdmul  22448  psdmvr  22451  coe1z  22543  coe1mul2lem1  22547  coe1tm  22553  coe1sclmul  22562  coe1sclmul2  22564  evls1sca  22602  evl1sca  22613  evls1fpws  22648  grpvrinv  22675  mdetunilem9  22896  matunitlindflem1  22955  pttoponconst  23877  cnmptc  23942  cnmptkc  23959  pt1hmeo  24086  tmdgsum2  24376  tsms0  24422  tgptsmscls  24430  resspwsds  24652  imasdsf1olem  24653  nmoeq0  25016  idnghm  25023  rrxcph  25674  ovolctb  25772  ovoliunnul  25789  vitalilem4  25893  vitalilem5  25894  ismbf  25910  mbfconst  25915  mbfss  25928  mbfmulc2re  25930  mbfneg  25932  mbfmulc2  25945  itg11  25973  itg2const  26022  itg2mulclem  26028  itg2mulc  26029  itg2monolem1  26032  itg0  26061  itgz  26062  itgvallem3  26067  iblposlem  26073  i1fibl  26089  itgitg1  26090  itgge0  26092  iblconst  26099  itgconst  26100  itgfsum  26108  iblmulc2  26112  itgmulc2lem1  26113  bddmulibl  26120  bddiblnc  26123  dvcmulf  26226  dvexp  26234  dvexp2  26235  dvmptid  26238  dvmptc  26239  dvef  26261  rolle  26271  dv11cn  26282  ftc1lem4  26320  ftc2  26325  tdeglem4  26339  ply1nzb  26402  plyconst  26485  plyeq0lem  26490  plypf1  26492  coeeulem  26504  plyco  26521  0dgr  26525  0dgrb  26526  dgrcolem2  26554  dgrco  26555  plymul02  26564  plymulidp  26566  plyremlem  26588  elqaalem3  26607  iaaOLD  26615  taylply2  26658  itgulm  26698  amgmlem  27280  lgam1  27354  ftalem7  27369  basellem8  27378  dchrfi  27545  dchrptlem3  27556  istrkg2ld  28855  bra0  32485  padct  33243  cshw1s2  33454  gsumind  33839  mplasclco  34081  selvply1rhmlem2  34086  selvply1rhm0  34091  extvfvcl  34101  mplvrpmmhm  34111  psrgsum  34113  psrmonprod  34117  esplyfval3  34137  fedgmullem2  34195  extdgfialglem2  34258  zar0ring  34443  xrge0mulc1cn  34506  esumnul  34613  esum0  34614  esumcvg  34651  ofcc  34671  mbfmcst  34825  sibf0  34900  0rrv  35017  ccatmulgnn0dir  35108  txsconnlem  35926  cvmliftphtlem  36003  faclim  36432  poimirlem30  38488  ovoliunnfl  38500  voliunnfl  38502  volsupnfl  38503  itg2addnclem  38509  iblmulc2nc  38523  itgmulc2nclem1  38524  itgmulc2nclem2  38525  itgmulc2nc  38526  itgabsnc  38527  ftc1cnnclem  38529  ftc1anclem3  38533  ftc1anclem5  38535  ftc1anclem7  38537  ftc1anclem8  38538  ftc2nc  38540  repwsmet  38688  rrnequiv  38689  fsuppssindlem2  43542  fsuppssind  43543  mzpconstmpt  43689  mzpcompact2lem  43700  mendlmod  44134  mendassa  44135  mnringmulrcld  45170  expgrowthi  45261  expgrowth  45263  binomcxplemrat  45278  binomcxplemnotnn0  45284  climconstmpt  46590  iblconstmpt  46888  iblempty  46897  itgiccshift  46912  itgperiod  46913  itgsbtaddcnst  46914  stoweidlem21  46953  hoicvr  47480  cjnpoly  47861  lindsrng01  49502  eufsn  49874  diag1a  50335  aacllem  50861  veroquadmodzerod  50906  amgmlemALT  50910