Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fconstg Structured version   Visualization version   GIF version

Theorem fconstg 6548
 Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004.)
Assertion
Ref Expression
fconstg (𝐵𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})

Proof of Theorem fconstg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sneq 4538 . . . 4 (𝑥 = 𝐵 → {𝑥} = {𝐵})
21xpeq2d 5553 . . 3 (𝑥 = 𝐵 → (𝐴 × {𝑥}) = (𝐴 × {𝐵}))
3 feq1 6476 . . . 4 ((𝐴 × {𝑥}) = (𝐴 × {𝐵}) → ((𝐴 × {𝑥}):𝐴⟶{𝑥} ↔ (𝐴 × {𝐵}):𝐴⟶{𝑥}))
4 feq3 6478 . . . 4 ({𝑥} = {𝐵} → ((𝐴 × {𝐵}):𝐴⟶{𝑥} ↔ (𝐴 × {𝐵}):𝐴⟶{𝐵}))
53, 4sylan9bb 513 . . 3 (((𝐴 × {𝑥}) = (𝐴 × {𝐵}) ∧ {𝑥} = {𝐵}) → ((𝐴 × {𝑥}):𝐴⟶{𝑥} ↔ (𝐴 × {𝐵}):𝐴⟶{𝐵}))
62, 1, 5syl2anc 587 . 2 (𝑥 = 𝐵 → ((𝐴 × {𝑥}):𝐴⟶{𝑥} ↔ (𝐴 × {𝐵}):𝐴⟶{𝐵}))
7 vex 3445 . . 3 𝑥 ∈ V
87fconst 6547 . 2 (𝐴 × {𝑥}):𝐴⟶{𝑥}
96, 8vtoclg 3516 1 (𝐵𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {csn 4528   × cxp 5521  ⟶wf 6328 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-v 3444  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-fun 6334  df-fn 6335  df-f 6336 This theorem is referenced by:  fnconstg  6549  fconst6g  6550  xpsng  6888  fvconst2g  6951  fconst2g  6952  symgpssefmnd  18537  xkoptsub  22300  mbfconstlem  24272  i1fmulclem  24347  i1fmulc  24348  itg2mulclem  24391  dvcmulf  24589  dvef  24624  coemulc  24896  resf1o  30536  locfinref  31260  ccatmulgnn0dir  31988  frlmvscadiccat  39595
 Copyright terms: Public domain W3C validator