### 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: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` and: `P ∧ Q` cand: `A 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