Theorem fconst6g 6774

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {csn 4594   × cxp 5664  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  fconst6  6775  map0g  8891  fdiagfn  8897  mapsncnv  8900  brwdom2  9545  cantnf0  9654  fseqdom  10029  pwsdiagel  17576  setcmon  18169  setcepi  18170  pwsmnd  18861  pws0g  18862  0mhm  18909  pwspjmhm  18920  pwsgrp  19149  pwsinvg  19150  symgpssefmnd  19497  pwscmn  19964  pwsabl  19965  pwsring  20438  pws1  20439  pwscrng  20440  pwslmod  21128  frlmlmod  21936  frlmlss  21938  psrvscacl  22138  psr0cl  22139  psrlmod  22146  mplsubglem  22185  evlsvvval  22281  coe1fval3  22405  coe1z  22461  coe1mul2  22467  coe1tm  22471  evls1sca  22520  rhmply1vsca  22582  mamuvs1  22599  mamuvs2  22600  lmconst  23455  cnconst2  23477  pwstps  23824  xkopt  23849  xkopjcn  23850  tmdgsum  24289  tmdgsum2  24290  symgtgp  24300  cstucnd  24477  imasdsf1olem  24567  pwsxms  24726  pwsms  24727  mbfconstlem  25823  mbfmulc2lem  25843  i1fmulc  25899  itg2mulc  25943  dvconst  26113  dvcmul  26140  plypf1  26406  amgmlem  27191  dchrelbas2  27438  resf1o  33112  elrspunidl  33767  ofcccat  34965  lpadlem1  35099  poimirlem28  38340  lflvscl  39892  lflvsdi1  39893  lflvsdi2  39894  lflvsass  39896  fsuppssind  43366  mhphf  43370  constmap  43485  mendlmod  43957  cantnfresb  44092  ofoafo  44124  naddcnffo  44132  naddcnfid1  44135  naddcnfid2  44136  onnoxpg  44196  dvsconst  45081  expgrowth  45086  mapssbi  45970  dvsinax  46668  amgmlemALT  50692