Theorem fconst6g 6234

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 6232	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		snssi 4472	. 2 ⊢ (𝐵 ∈ 𝐶 → {𝐵} ⊆ 𝐶)
3	1, 2	fssd 6197	1 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∈ wcel 2144  {csn 4314   × cxp 5247  ⟶wf 6027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-fun 6033  df-fn 6034  df-f 6035

This theorem is referenced by:  fconst6  6235  map0g  8049  fdiagfn  8054  mapsncnv  8057  brwdom2  8633  cantnf0  8735  fseqdom  9048  pwsdiagel  16364  setcmon  16943  setcepi  16944  pwsmnd  17532  pws0g  17533  0mhm  17565  pwspjmhm  17575  pwsgrp  17734  pwsinvg  17735  pwscmn  18472  pwsabl  18473  pwsring  18822  pws1  18823  pwscrng  18824  pwslmod  19182  psrvscacl  19607  psr0cl  19608  psrlmod  19615  mplsubglem  19648  coe1fval3  19792  coe1z  19847  coe1mul2  19853  coe1tm  19857  evls1sca  19902  frlmlmod  20309  frlmlss  20311  mamuvs1  20427  mamuvs2  20428  lmconst  21285  cnconst2  21307  pwstps  21653  xkopt  21678  xkopjcn  21679  tmdgsum  22118  tmdgsum2  22119  symgtgp  22124  cstucnd  22307  imasdsf1olem  22397  pwsxms  22556  pwsms  22557  mbfconstlem  23614  mbfmulc2lem  23633  i1fmulc  23689  itg2mulc  23733  dvconst  23899  dvcmul  23926  plypf1  24187  amgmlem  24936  dchrelbas2  25182  resf1o  29839  ofcccat  30954  poimirlem28  33763  lflvscl  34879  lflvsdi1  34880  lflvsdi2  34881  lflvsass  34883  constmap  37795  mendlmod  38282  dvsconst  39048  expgrowth  39053  mapssbi  39917  dvsinax  40639  amgmlemALT  43070