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