Nuprl Lemma : free-from-atom_wf_general
∀[T:Type]. ∀[x:T]. ∀[a:Atom$m].  (a#x:T ∈ ℙ)
Proof
Definitions occuring in Statement : 
free-from-atom: a#x:T
, 
atom: Atom$n
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
member: t ∈ T
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
prop: ℙ
Rules used in proof : 
universeEquality, 
hypothesisEquality, 
Error :universeIsType, 
Error :isect_memberFormation_alt, 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalSubstitution, 
equalitySymmetry, 
hypothesis, 
equalityTransitivity, 
axiomEquality, 
sqequalHypSubstitution, 
sqequalRule, 
cut, 
introduction, 
freeFromAtomEquality, 
atomnEquality
Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[a:Atom\$m].    (a\#x:T  \mmember{}  \mBbbP{})
Date html generated:
2019_06_20-AM-11_20_18
Last ObjectModification:
2018_10_15-PM-10_13_42
Theory : atom_1
Home
Index