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

Syntax hints:   → wi 4   ∈ wcel 2114  {csn 4517   × cxp 5524  ⟶wf 6336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pr 5297

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-v 3401  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5430  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-fun 6342  df-fn 6343  df-f 6344

This theorem is referenced by:  fconst6  6569  map0g  8497  fdiagfn  8503  mapsncnv  8506  brwdom2  9113  cantnf0  9214  fseqdom  9529  pwsdiagel  16876  setcmon  17462  setcepi  17463  pwsmnd  18065  pws0g  18066  0mhm  18103  pwspjmhm  18113  pwsgrp  18332  pwsinvg  18333  symgpssefmnd  18645  pwscmn  19105  pwsabl  19106  pwsring  19490  pws1  19491  pwscrng  19492  pwslmod  19864  frlmlmod  20568  frlmlss  20570  psrvscacl  20775  psr0cl  20776  psrlmod  20783  mplsubglem  20818  coe1fval3  20986  coe1z  21041  coe1mul2  21047  coe1tm  21051  evls1sca  21096  mamuvs1  21159  mamuvs2  21160  lmconst  22015  cnconst2  22037  pwstps  22384  xkopt  22409  xkopjcn  22410  tmdgsum  22849  tmdgsum2  22850  symgtgp  22860  cstucnd  23039  imasdsf1olem  23129  pwsxms  23288  pwsms  23289  mbfconstlem  24382  mbfmulc2lem  24402  i1fmulc  24459  itg2mulc  24503  dvconst  24672  dvcmul  24699  plypf1  24964  amgmlem  25730  dchrelbas2  25976  resf1o  30643  elrspunidl  31181  ofcccat  32095  lpadlem1  32230  poimirlem28  35451  lflvscl  36737  lflvsdi1  36738  lflvsdi2  36739  lflvsass  36741  evlsbagval  39877  fsuppssind  39884  mhphf  39887  constmap  40130  mendlmod  40613  dvsconst  41509  expgrowth  41514  mapssbi  42314  dvsinax  43019  amgmlemALT  45990