Nuprl Lemma : uiff_weakening

[P:ℙ]. (SqStable(P)  {uiff(P;P)})


Proof




Definitions occuring in Statement :  sq_stable: SqStable(P) uiff: uiff(P;Q) uall: [x:A]. B[x] prop: guard: {T} implies:  Q
Definitions unfolded in proof :  guard: {T} sq_stable: SqStable(P) implies:  Q member: t ∈ T squash: T uall: [x:A]. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a prop:
Lemmas referenced :  sq_stable_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut hypothesis sqequalHypSubstitution independent_functionElimination thin introduction imageMemberEquality hypothesisEquality baseClosed imageElimination isect_memberFormation lambdaFormation independent_pairFormation because_Cache lemma_by_obid isectElimination universeEquality

Latex:
\mforall{}[P:\mBbbP{}].  (SqStable(P)  {}\mRightarrow{}  \{uiff(P;P)\})



Date html generated: 2016_05_13-PM-03_10_10
Last ObjectModification: 2016_01_06-PM-05_48_01

Theory : core_2


Home Index