Nuprl Lemma : PZF-safe-Fvs-subset
∀C:Type. ∀phi:Form(C). ∀vs:Atom List. (PZF-safe(phi;vs) ⇒ l_subset(Atom;vs;FormFvs(phi)))
Proof
Definitions occuring in Statement :
PZF-safe: PZF-safe(phi;vs),
FormFvs: FormFvs(f),
Form: Form(C),
l_subset: l_subset(T;as;bs),
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q,
atom: Atom,
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
FormSafe1: FormSafe1(f),
Form_ind: Form_ind,
PZF-safe: PZF-safe(phi;vs),
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
FormSafe1-Fvs-subset,
PZF-safe_wf,
list_wf,
Form_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
isectElimination,
cumulativity,
atomEquality,
universeEquality
Latex:
\mforall{}C:Type. \mforall{}phi:Form(C). \mforall{}vs:Atom List. (PZF-safe(phi;vs) {}\mRightarrow{} l\_subset(Atom;vs;FormFvs(phi)))
Date html generated:
2018_05_21-PM-11_29_03
Last ObjectModification:
2017_10_12-PM-00_08_45
Theory : PZF
Home
Index