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 𝑆 = ( 𝑥C ↦ ( ( proj𝑥 ) ‘ 𝑢 ) )
Assertion hstrlem2 ( 𝐶C → ( 𝑆𝐶 ) = ( ( proj𝐶 ) ‘ 𝑢 ) )

Proof

Step Hyp Ref Expression
1 hstrlem2.1 𝑆 = ( 𝑥C ↦ ( ( proj𝑥 ) ‘ 𝑢 ) )
2 fveq2 ( 𝑥 = 𝐶 → ( proj𝑥 ) = ( proj𝐶 ) )
3 2 fveq1d ( 𝑥 = 𝐶 → ( ( proj𝑥 ) ‘ 𝑢 ) = ( ( proj𝐶 ) ‘ 𝑢 ) )
4 fvex ( ( proj𝐶 ) ‘ 𝑢 ) ∈ V
5 3 1 4 fvmpt ( 𝐶C → ( 𝑆𝐶 ) = ( ( proj𝐶 ) ‘ 𝑢 ) )