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

Theorem fconst6g 5988
Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Assertion
Ref Expression
fconst6g (𝐵𝐶 → (𝐴 × {𝐵}):𝐴𝐶)

Proof of Theorem fconst6g
StepHypRef Expression
1 fconstg 5986 . 2 (𝐵𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2 snssi 4275 . 2 (𝐵𝐶 → {𝐵} ⊆ 𝐶)
31, 2fssd 5952 1 (𝐵𝐶 → (𝐴 × {𝐵}):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1975  {csn 4120   × cxp 5022  wf 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-mpt 4635  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-fun 5788  df-fn 5789  df-f 5790
This theorem is referenced by:  fconst6  5989  map0g  7756  fdiagfn  7760  mapsncnv  7763  brwdom2  8334  cantnf0  8428  fseqdom  8705  pwsdiagel  15922  setcmon  16502  setcepi  16503  pwsmnd  17090  pws0g  17091  0mhm  17123  pwspjmhm  17133  pwsgrp  17292  pwsinvg  17293  pwscmn  18031  pwsabl  18032  pwsring  18380  pws1  18381  pwscrng  18382  pwslmod  18733  psrvscacl  19156  psr0cl  19157  psrlmod  19164  mplsubglem  19197  coe1fval3  19341  coe1z  19396  coe1mul2  19402  coe1tm  19406  evls1sca  19451  frlmlmod  19850  frlmlss  19852  mamuvs1  19968  mamuvs2  19969  lmconst  20813  cnconst2  20835  pwstps  21181  xkopt  21206  xkopjcn  21207  tmdgsum  21647  tmdgsum2  21648  symgtgp  21653  cstucnd  21836  imasdsf1olem  21925  pwsxms  22084  pwsms  22085  mbfconstlem  23115  mbfmulc2lem  23133  i1fmulc  23189  itg2mulc  23233  dvconst  23399  dvcmul  23426  plypf1  23685  amgmlem  24429  dchrelbas2  24675  resf1o  28695  ofcccat  29748  poimirlem28  32406  lflvscl  33181  lflvsdi1  33182  lflvsdi2  33183  lflvsass  33185  constmap  36093  mendlmod  36581  dvsconst  37350  expgrowth  37355  mapssbi  38199  dvsinax  38601  amgmlemALT  42317
  Copyright terms: Public domain W3C validator