Nuprl Lemma : classical-exists1

[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] exists: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q exists: x:A. B[x] prop: so_lambda: λ2x.t[x] so_apply: x[s] classical: {P} unit: Unit
Lemmas referenced :  it_wf classical_wf exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis dependent_functionElimination setElimination rename dependent_set_memberEquality axiomEquality natural_numberEquality functionEquality cumulativity universeEquality isect_memberEquality because_Cache dependent_pairFormation

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



Date html generated: 2016_05_13-PM-03_16_56
Last ObjectModification: 2016_01_06-PM-05_20_41

Theory : core_2


Home Index