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

Theorem fconst6g 6561
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 6559 . 2 (𝐵𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2 snssi 4733 . 2 (𝐵𝐶 → {𝐵} ⊆ 𝐶)
31, 2fssd 6521 1 (𝐵𝐶 → (𝐴 × {𝐵}):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  {csn 4557   × cxp 5546  wf 6344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-fun 6350  df-fn 6351  df-f 6352
This theorem is referenced by:  fconst6  6562  map0g  8437  fdiagfn  8442  mapsncnv  8445  brwdom2  9025  cantnf0  9126  fseqdom  9440  pwsdiagel  16758  setcmon  17335  setcepi  17336  pwsmnd  17934  pws0g  17935  0mhm  17972  pwspjmhm  17982  pwsgrp  18149  pwsinvg  18150  pwscmn  18912  pwsabl  18913  pwsring  19294  pws1  19295  pwscrng  19296  pwslmod  19671  psrvscacl  20101  psr0cl  20102  psrlmod  20109  mplsubglem  20142  coe1fval3  20304  coe1z  20359  coe1mul2  20365  coe1tm  20369  evls1sca  20414  frlmlmod  20821  frlmlss  20823  mamuvs1  20942  mamuvs2  20943  lmconst  21797  cnconst2  21819  pwstps  22166  xkopt  22191  xkopjcn  22192  tmdgsum  22631  tmdgsum2  22632  symgtgp  22637  cstucnd  22820  imasdsf1olem  22910  pwsxms  23069  pwsms  23070  mbfconstlem  24155  mbfmulc2lem  24175  i1fmulc  24231  itg2mulc  24275  dvconst  24441  dvcmul  24468  plypf1  24729  amgmlem  25494  dchrelbas2  25740  resf1o  30392  ofcccat  31712  lpadlem1  31847  poimirlem28  34801  lflvscl  36093  lflvsdi1  36094  lflvsdi2  36095  lflvsass  36097  constmap  39188  mendlmod  39671  dvsconst  40539  expgrowth  40544  mapssbi  41352  dvsinax  42073  amgmlemALT  44832
  Copyright terms: Public domain W3C validator