MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fconstg Structured version   Unicode version

Theorem fconstg 5590
Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004.)
Assertion
Ref Expression
fconstg  |-  ( B  e.  V  ->  ( A  X.  { B }
) : A --> { B } )

Proof of Theorem fconstg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 sneq 3880 . . . 4  |-  ( x  =  B  ->  { x }  =  { B } )
21xpeq2d 4856 . . 3  |-  ( x  =  B  ->  ( A  X.  { x }
)  =  ( A  X.  { B }
) )
3 feq1 5535 . . . 4  |-  ( ( A  X.  { x } )  =  ( A  X.  { B } )  ->  (
( A  X.  {
x } ) : A --> { x }  <->  ( A  X.  { B } ) : A --> { x } ) )
4 feq3 5537 . . . 4  |-  ( { x }  =  { B }  ->  ( ( A  X.  { B } ) : A --> { x }  <->  ( A  X.  { B } ) : A --> { B } ) )
53, 4sylan9bb 699 . . 3  |-  ( ( ( A  X.  {
x } )  =  ( A  X.  { B } )  /\  {
x }  =  { B } )  ->  (
( A  X.  {
x } ) : A --> { x }  <->  ( A  X.  { B } ) : A --> { B } ) )
62, 1, 5syl2anc 661 . 2  |-  ( x  =  B  ->  (
( A  X.  {
x } ) : A --> { x }  <->  ( A  X.  { B } ) : A --> { B } ) )
7 vex 2969 . . 3  |-  x  e. 
_V
87fconst 5589 . 2  |-  ( A  X.  { x }
) : A --> { x }
96, 8vtoclg 3023 1  |-  ( B  e.  V  ->  ( A  X.  { B }
) : A --> { B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    e. wcel 1756   {csn 3870    X. cxp 4830   -->wf 5407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pr 4524
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-fun 5413  df-fn 5414  df-f 5415
This theorem is referenced by:  fnconstg  5591  fconst6g  5592  xpsng  5877  fvconst2g  5924  fconst2g  5925  xkoptsub  19196  mbfconstlem  21076  i1fmulclem  21149  i1fmulc  21150  itg2mulclem  21193  dvcmulf  21388  dvef  21421  coemulc  21691  resf1o  25975  ccatmulgnn0dir  26888
  Copyright terms: Public domain W3C validator