Nuprl Lemma : anyprop_wf
anyprop() ∈ ℙ
Proof
Definitions occuring in Statement :
anyprop: anyprop(),
prop: ℙ,
member: t ∈ T
Definitions unfolded in proof :
anyprop: anyprop(),
member: t ∈ T
Lemmas referenced :
false_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
lemma_by_obid,
hypothesis
Latex:
anyprop() \mmember{} \mBbbP{}
Date html generated:
2016_05_15-PM-07_21_27
Last ObjectModification:
2015_12_27-AM-11_27_04
Theory : general
Home
Index