Theorem fconstmpt 5723

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 4604	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 634	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 5177	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5667	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 5192	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2794	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 400   = wceq 1568   ∈ wcel 2141  {csn 4588  {copab 5172   ↦ cmpt 5191   × cxp 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-sn 4589  df-opab 5173  df-mpt 5192  df-xp 5667

This theorem is referenced by:  fconst  6764  fcoconst  7130  fmptsn  7165  rnmptc  7205  fconstmpo  7527  ofc12  7704  caofinvl  7706  caofidlcan  7712  xpexgALT  7977  cantnf  9661  cnfcom2lem  9669  repsconst  14808  harmonic  15912  geomulcvg  15929  vdwlem8  17047  ramcl  17088  pwsvscafval  17547  setcepi  18144  diag2  18300  pws0g  18830  smndex1gbas  18960  smndex1gid  18962  smndex1igid  18964  smndex1igidOLD  18965  0frgp  19848  pwsgsum  20051  rrgsupp  20785  lmhmvsca  21145  uvcresum  21922  psrlinv  22084  psrlidm  22090  psrridm  22091  psrass23l  22095  psrass23  22097  mplcoe1  22167  mplcoe3  22168  mplcoe5  22170  mplmon2  22191  evlslem2  22209  evlslem1  22212  evlsvvval  22223  mhpsclcl  22289  psdmul  22308  psdmvr  22311  coe1z  22403  coe1mul2lem1  22407  coe1tm  22413  coe1sclmul  22422  coe1sclmul2  22424  evls1sca  22462  evl1sca  22473  evls1fpws  22508  grpvrinv  22535  mdetunilem9  22756  pttoponconst  23733  cnmptc  23798  cnmptkc  23815  pt1hmeo  23942  tmdgsum2  24232  tsms0  24278  tgptsmscls  24286  resspwsds  24508  imasdsf1olem  24509  nmoeq0  24872  idnghm  24879  rrxcph  25530  ovolctb  25628  ovoliunnul  25645  vitalilem4  25749  vitalilem5  25750  ismbf  25766  mbfconst  25771  mbfss  25784  mbfmulc2re  25786  mbfneg  25788  mbfmulc2  25801  itg11  25829  itg2const  25878  itg2mulclem  25884  itg2mulc  25885  itg2monolem1  25888  itg0  25918  itgz  25919  itgvallem3  25924  iblposlem  25930  i1fibl  25946  itgitg1  25947  itgge0  25949  iblconst  25956  itgconst  25957  itgfsum  25965  iblmulc2  25969  itgmulc2lem1  25970  bddmulibl  25977  bddiblnc  25980  dvcmulf  26083  dvexp  26091  dvexp2  26092  dvmptid  26095  dvmptc  26096  dvef  26118  rolle  26128  dv11cn  26139  ftc1lem4  26177  ftc2  26182  tdeglem4  26196  ply1nzb  26259  plyconst  26342  plyeq0lem  26346  plypf1  26348  coeeulem  26360  plyco  26377  0dgr  26381  0dgrb  26382  dgrcolem2  26410  dgrco  26411  plymul02  26420  plymulidp  26422  plyremlem  26444  elqaalem3  26461  iaa  26465  taylply2  26507  itgulm  26547  amgmlem  27130  lgam1  27204  ftalem7  27219  basellem8  27228  dchrfi  27395  dchrptlem3  27406  istrkg2ld  28705  bra0  32268  padct  33029  cshw1s2  33246  gsumind  33631  mplasclco  33872  selvply1rhmlem2  33877  selvply1rhm0  33882  extvfvcl  33892  mplvrpmmhm  33902  psrgsum  33904  psrmonprod  33908  esplyfval3  33928  fedgmullem2  33986  extdgfialglem2  34049  zar0ring  34234  xrge0mulc1cn  34297  esumnul  34404  esum0  34405  esumcvg  34442  ofcc  34462  mbfmcst  34615  sibf0  34690  0rrv  34807  ccatmulgnn0dir  34898  txsconnlem  35686  cvmliftphtlem  35763  faclim  36192  matunitlindflem1  38211  poimirlem30  38245  ovoliunnfl  38257  voliunnfl  38259  volsupnfl  38260  itg2addnclem  38266  iblmulc2nc  38280  itgmulc2nclem1  38281  itgmulc2nclem2  38282  itgmulc2nc  38283  itgabsnc  38284  ftc1cnnclem  38286  ftc1anclem3  38290  ftc1anclem5  38292  ftc1anclem7  38294  ftc1anclem8  38295  ftc2nc  38297  repwsmet  38429  rrnequiv  38430  fsuppssindlem2  43272  fsuppssind  43273  mzpconstmpt  43419  mzpcompact2lem  43430  mendlmod  43864  mendassa  43865  mnringmulrcld  44900  expgrowthi  44991  expgrowth  44993  binomcxplemrat  45008  binomcxplemnotnn0  45014  climconstmpt  46320  iblconstmpt  46618  iblempty  46627  itgiccshift  46642  itgperiod  46643  itgsbtaddcnst  46644  stoweidlem21  46683  hoicvr  47210  nthrucw  47550  cjnpoly  47571  lindsrng01  49193  eufsn  49565  diag1a  50028  aacllem  50546  amgmlemALT  50548