Nuprl Lemma : test-evd2

[D:ℙ]. ∀[P,Q:D ⟶ ℙ].  ((∀x:D. ((P x)  (Q x)))  (∃x:D. (P x))  (∃x:D. (Q x)))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: all: x:A. B[x] exists: x:A. B[x] implies:  Q apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] prop: so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q exists: x:A. B[x] all: x:A. B[x]
Lemmas referenced :  exists_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity hypothesisEquality applyEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality hypothesis functionEquality isect_memberFormation lambdaFormation rename productElimination dependent_pairFormation dependent_functionElimination independent_functionElimination because_Cache cumulativity universeEquality

Latex:
\mforall{}[D:\mBbbP{}].  \mforall{}[P,Q:D  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:D.  ((P  x)  {}\mRightarrow{}  (Q  x)))  {}\mRightarrow{}  (\mexists{}x:D.  (P  x))  {}\mRightarrow{}  (\mexists{}x:D.  (Q  x)))



Date html generated: 2016_05_15-PM-03_18_49
Last ObjectModification: 2015_12_27-PM-01_03_20

Theory : general


Home Index