Nuprl Lemma : not_wf

[A:ℙ]. A ∈ ℙ)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: not: ¬A member: t ∈ T
Definitions unfolded in proof :  not: ¬A uall: [x:A]. B[x] member: t ∈ T implies:  Q prop:
Lemmas referenced :  false_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut functionEquality sqequalHypSubstitution hypothesisEquality lemma_by_obid hypothesis axiomEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[A:\mBbbP{}].  (\mneg{}A  \mmember{}  \mBbbP{})



Date html generated: 2016_05_13-PM-03_08_02
Last ObjectModification: 2016_01_06-PM-05_27_53

Theory : core_2


Home Index