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

Theorem fconst6g 6732
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 6730 . 2 (𝐵𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2 snssi 4769 . 2 (𝐵𝐶 → {𝐵} ⊆ 𝐶)
31, 2fssd 6687 1 (𝐵𝐶 → (𝐴 × {𝐵}):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  {csn 4587   × cxp 5632  wf 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  fconst6  6733  map0g  8823  fdiagfn  8829  mapsncnv  8832  brwdom2  9510  cantnf0  9612  fseqdom  9963  pwsdiagel  17380  setcmon  17974  setcepi  17975  pwsmnd  18592  pws0g  18593  0mhm  18631  pwspjmhm  18641  pwsgrp  18860  pwsinvg  18861  symgpssefmnd  19178  pwscmn  19642  pwsabl  19643  pwsring  20040  pws1  20041  pwscrng  20042  pwslmod  20434  frlmlmod  21158  frlmlss  21160  psrvscacl  21364  psr0cl  21365  psrlmod  21373  mplsubglem  21408  coe1fval3  21582  coe1z  21637  coe1mul2  21643  coe1tm  21647  evls1sca  21692  mamuvs1  21755  mamuvs2  21756  lmconst  22615  cnconst2  22637  pwstps  22984  xkopt  23009  xkopjcn  23010  tmdgsum  23449  tmdgsum2  23450  symgtgp  23460  cstucnd  23639  imasdsf1olem  23729  pwsxms  23891  pwsms  23892  mbfconstlem  24994  mbfmulc2lem  25014  i1fmulc  25071  itg2mulc  25115  dvconst  25284  dvcmul  25311  plypf1  25576  amgmlem  26342  dchrelbas2  26588  resf1o  31650  elrspunidl  32206  ofcccat  33158  lpadlem1  33293  poimirlem28  36109  lflvscl  37542  lflvsdi1  37543  lflvsdi2  37544  lflvsass  37546  evlsbagval  40751  fsuppssind  40771  mhphf  40774  constmap  41039  mendlmod  41523  cantnfresb  41661  ofoafo  41673  naddcnffo  41681  naddcnfid1  41684  naddcnfid2  41685  onnog  41708  dvsconst  42617  expgrowth  42622  mapssbi  43441  dvsinax  44161  amgmlemALT  47257
  Copyright terms: Public domain W3C validator