At: valuation wf 1 1 5
1. Q: Formula
Prop
2. 
F:{F:Formula| Q(F) }, a:Assignment. (F under a) 
3. y2: {F:Formula| Q(F) }
4. y3: Formula
5. Q(y3)
6. a: Assignment
(y2 under a) 
(y3 under a)
By:
MemberEqCD
THEN
HypBackchain
Generated subgoals:None
About:
