Nuprl Lemma : classical-all

[T:Type]. ∀[P:T ⟶ ℙ].  (∀x:T. {P[x]} ⇐⇒ {∀x:T. {P[x]}})


Proof




Definitions occuring in Statement :  classical: {P} uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q implies:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q all: x:A. B[x] classical: {P} unit: Unit subtype_rel: A ⊆B guard: {T}
Lemmas referenced :  it_wf classical_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis productElimination independent_pairEquality dependent_functionElimination dependent_set_memberEquality axiomEquality natural_numberEquality setElimination rename universeEquality functionEquality cumulativity isect_memberEquality because_Cache

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    (\mforall{}x:T.  \{P[x]\}  \mLeftarrow{}{}\mRightarrow{}  \{\mforall{}x:T.  \{P[x]\}\})



Date html generated: 2016_05_13-PM-03_17_06
Last ObjectModification: 2016_01_06-PM-05_21_04

Theory : core_2


Home Index