Metamath Proof Explorer

Theorem hstrlem2

Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis hstrlem2.1 
|- S = ( x e. CH |-> ( ( projh ` x ) ` u ) )
Assertion hstrlem2 
|- ( C e. CH -> ( S ` C ) = ( ( projh ` C ) ` u ) )

Proof

Step Hyp Ref Expression
1 hstrlem2.1 
 |-  S = ( x e. CH |-> ( ( projh ` x ) ` u ) )
2 fveq2 
 |-  ( x = C -> ( projh ` x ) = ( projh ` C ) )
3 2 fveq1d 
 |-  ( x = C -> ( ( projh ` x ) ` u ) = ( ( projh ` C ) ` u ) )
4 fvex 
 |-  ( ( projh ` C ) ` u ) e. _V
5 3 1 4 fvmpt 
 |-  ( C e. CH -> ( S ` C ) = ( ( projh ` C ) ` u ) )