Theorem fconstmpt 5333

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 4350	. . . 4 ⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
2	1	anbi2i 616	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
3	2	opabbii 4876	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4		df-xp 5283	. 2 ⊢ (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝐵})}
5		df-mpt 4889	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	3, 4, 5	3eqtr4i 2797	1 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 384   = wceq 1652   ∈ wcel 2155  {csn 4334  {copab 4871   ↦ cmpt 4888   × cxp 5275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-sn 4335  df-opab 4872  df-mpt 4889  df-xp 5283

This theorem is referenced by:  fconst  6273  fcoconst  6592  fmptsn  6626  fconstmpt2  6953  ofc12  7120  caofinvl  7122  xpexgALT  7359  cantnf  8805  cnfcom2lem  8813  repsconst  13796  harmonic  14875  geomulcvg  14891  vdwlem8  15971  ramcl  16012  pwsvscafval  16420  setcepi  17003  diag2  17151  pws0g  17592  0frgp  18458  pwsgsum  18644  lmhmvsca  19317  rrgsupp  19565  psrlinv  19671  psrlidm  19677  psrridm  19678  psrass23l  19682  psrass23  19684  mplcoe1  19739  mplcoe3  19740  mplcoe5  19742  mplmon2  19766  evlslem2  19785  evlslem1  19788  coe1z  19906  coe1mul2lem1  19910  coe1tm  19916  coe1sclmul  19925  coe1sclmul2  19927  evls1sca  19961  evl1sca  19971  uvcresum  20408  grpvrinv  20478  mdetunilem9  20703  pttoponconst  21680  cnmptc  21745  cnmptkc  21762  pt1hmeo  21889  tmdgsum2  22179  tsms0  22224  tgptsmscls  22232  resspwsds  22456  imasdsf1olem  22457  nmoeq0  22819  idnghm  22826  rrxcph  23469  ovolctb  23548  ovoliunnul  23565  vitalilem4  23669  vitalilem5  23670  ismbf  23686  mbfconst  23691  mbfss  23704  mbfmulc2re  23706  mbfneg  23708  mbfmulc2  23721  itg11  23749  itg2const  23798  itg2mulclem  23804  itg2mulc  23805  itg2monolem1  23808  itg0  23837  itgz  23838  itgvallem3  23843  iblposlem  23849  i1fibl  23865  itgitg1  23866  itgge0  23868  iblconst  23875  itgconst  23876  itgfsum  23884  iblmulc2  23888  itgmulc2lem1  23889  bddmulibl  23896  dvcmulf  23999  dvexp  24007  dvexp2  24008  dvmptid  24011  dvmptc  24012  dvef  24034  rolle  24044  dv11cn  24055  ftc1lem4  24093  ftc2  24098  tdeglem4  24111  ply1nzb  24173  plyconst  24253  plyeq0lem  24257  plypf1  24259  coeeulem  24271  plyco  24288  0dgr  24292  0dgrb  24293  dgrcolem2  24321  dgrco  24322  plyremlem  24350  elqaalem3  24367  iaa  24371  taylply2  24413  itgulm  24453  amgmlem  25007  lgam1  25081  ftalem7  25096  basellem8  25105  dchrfi  25271  dchrptlem3  25282  bra0  29265  padct  29946  xrge0mulc1cn  30434  esumnul  30557  esum0  30558  esumcvg  30595  ofcc  30615  mbfmcst  30768  sibf0  30843  0rrv  30961  ccatmulgnn0dir  31068  plymul02  31072  plymulx  31074  txsconnlem  31670  cvmliftphtlem  31747  faclim  32077  matunitlindflem1  33829  poimirlem30  33863  ovoliunnfl  33875  voliunnfl  33877  volsupnfl  33878  itg2addnclem  33884  iblmulc2nc  33898  itgmulc2nclem1  33899  itgmulc2nclem2  33900  itgmulc2nc  33901  itgabsnc  33902  bddiblnc  33903  ftc1cnnclem  33906  ftc1anclem3  33910  ftc1anclem5  33912  ftc1anclem7  33914  ftc1anclem8  33915  ftc2nc  33917  repwsmet  34055  rrnequiv  34056  mzpconstmpt  37981  mzpcompact2lem  37992  mendlmod  38440  mendassa  38441  expgrowthi  39206  expgrowth  39208  binomcxplemrat  39223  binomcxplemnotnn0  39229  rnmptc  40000  climconstmpt  40528  iblconstmpt  40809  iblempty  40818  itgiccshift  40833  itgperiod  40834  itgsbtaddcnst  40835  stoweidlem21  40875  lindsrng01  42926  aacllem  43219  amgmlemALT  43221