Theorem fconst6g 6568

Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Assertion

Ref	Expression
fconst6g	⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶)

Proof of Theorem fconst6g

Step	Hyp	Ref	Expression
1		fconstg 6566	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		snssi 4741	. 2 ⊢ (𝐵 ∈ 𝐶 → {𝐵} ⊆ 𝐶)
3	1, 2	fssd 6528	1 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∈ wcel 2114  {csn 4567   × cxp 5553  ⟶wf 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-fun 6357  df-fn 6358  df-f 6359

This theorem is referenced by:  fconst6  6569  map0g  8448  fdiagfn  8454  mapsncnv  8457  brwdom2  9037  cantnf0  9138  fseqdom  9452  pwsdiagel  16770  setcmon  17347  setcepi  17348  pwsmnd  17946  pws0g  17947  0mhm  17984  pwspjmhm  17994  pwsgrp  18211  pwsinvg  18212  symgpssefmnd  18524  pwscmn  18983  pwsabl  18984  pwsring  19365  pws1  19366  pwscrng  19367  pwslmod  19742  psrvscacl  20173  psr0cl  20174  psrlmod  20181  mplsubglem  20214  coe1fval3  20376  coe1z  20431  coe1mul2  20437  coe1tm  20441  evls1sca  20486  frlmlmod  20893  frlmlss  20895  mamuvs1  21014  mamuvs2  21015  lmconst  21869  cnconst2  21891  pwstps  22238  xkopt  22263  xkopjcn  22264  tmdgsum  22703  tmdgsum2  22704  symgtgp  22714  cstucnd  22893  imasdsf1olem  22983  pwsxms  23142  pwsms  23143  mbfconstlem  24228  mbfmulc2lem  24248  i1fmulc  24304  itg2mulc  24348  dvconst  24514  dvcmul  24541  plypf1  24802  amgmlem  25567  dchrelbas2  25813  resf1o  30466  ofcccat  31813  lpadlem1  31948  poimirlem28  34935  lflvscl  36228  lflvsdi1  36229  lflvsdi2  36230  lflvsass  36232  constmap  39330  mendlmod  39813  dvsconst  40682  expgrowth  40687  mapssbi  41496  dvsinax  42217  amgmlemALT  44924