Nuprl Lemma : prob2.4

[U:Type]. ∀[P,Q:U ⟶ ℙ].  ((∃x:U. ((P x) ∧ (Q x)))  ((∃x:U. (P x)) ∧ (∃x:U. (Q x))))


Proof




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

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



Date html generated: 2016_05_15-PM-07_43_51
Last ObjectModification: 2015_12_27-AM-11_11_29

Theory : general


Home Index