### Nuprl Lemma : uni_sat_wf

`∀[T:Type]. ∀[a:T]. ∀[Q:T ⟶ ℙ].  (a = !x:T. Q[x] ∈ ℙ)`

Proof

Definitions occuring in Statement :  uni_sat: `a = !x:T. Q[x]` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uni_sat: `a = !x:T. Q[x]` prop: `ℙ` and: `P ∧ Q` so_apply: `x[s]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  all_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule productEquality applyEquality hypothesisEquality hypothesis thin lambdaEquality sqequalHypSubstitution universeEquality extract_by_obid isectElimination functionEquality axiomEquality equalityTransitivity equalitySymmetry Error :functionIsType,  Error :inhabitedIsType,  Error :universeIsType,  isect_memberEquality cumulativity because_Cache

Latex:
\mforall{}[T:Type].  \mforall{}[a:T].  \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].    (a  =  !x:T.  Q[x]  \mmember{}  \mBbbP{})

Date html generated: 2019_06_20-AM-11_18_10
Last ObjectModification: 2018_09_26-AM-10_25_16

Theory : core_2

Home Index