PrintForm Definitions valuation Sections ClassicalProps(jlc) Doc

At: valuation wf 1 1 2
1. Q: FormulaProp
2. F:{F:Formula| Q(F) }, a:Assignment. (F under a)
3. x: Formula
4. Q(x)
5. a: Assignment

(x under a)
By:
MemberEqCD
THEN
HypBackchain
Generated subgoals:

None

About:
memberfunctionpropallsetapply