Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fconstmpt GIF version

Theorem fconstmpt 4626
 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.
StepHypRef Expression
1 velsn 3573 . . . 4 (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵)
21anbi2i 453 . . 3 ((𝑥𝐴𝑦 ∈ {𝐵}) ↔ (𝑥𝐴𝑦 = 𝐵))
32opabbii 4027 . 2 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
4 df-xp 4585 . 2 (𝐴 × {𝐵}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ {𝐵})}
5 df-mpt 4023 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
63, 4, 53eqtr4i 2185 1 (𝐴 × {𝐵}) = (𝑥𝐴𝐵)
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   = wceq 1332   ∈ wcel 2125  {csn 3556  {copab 4020   ↦ cmpt 4021   × cxp 4577 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-v 2711  df-sn 3562  df-opab 4022  df-mpt 4023  df-xp 4585 This theorem is referenced by:  fconst  5358  fcoconst  5631  fmptsn  5649  fconstmpo  5906  ofc12  6042  caofinvl  6044  xpexgALT  6071  inftonninf  10318  fser0const  10393  prod1dc  11460  cnmptc  12621  dvexp  13014  dvexp2  13015  dvmptidcn  13017  dvmptccn  13018  dvef  13027  nninfall  13522  nninfsellemeqinf  13529  exmidsbthrlem  13534
 Copyright terms: Public domain W3C validator