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 C proj x u
Assertion hstrlem2 C C S C = proj C u

Proof

Step Hyp Ref Expression
1 hstrlem2.1 S = x C proj x u
2 fveq2 x = C proj x = proj C
3 2 fveq1d x = C proj x u = proj C u
4 fvex proj C u V
5 3 1 4 fvmpt C C S C = proj C u