### Nuprl Lemma : respects-equality-set-trivial

`∀[T:Type]. ∀[P:T ⟶ ℙ].  respects-equality(T;{x:T| P[x]} )`

Proof

Definitions occuring in Statement :  respects-equality: `respects-equality(S;T)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` respects-equality: `respects-equality(S;T)` all: `∀x:A. B[x]` implies: `P `` Q` squash: `↓T` prop: `ℙ` so_apply: `x[s]`
Lemmas referenced :  istype-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :lambdaFormation_alt,  sqequalHypSubstitution equalityTransitivity hypothesis equalitySymmetry applyLambdaEquality setElimination thin rename sqequalRule imageMemberEquality hypothesisEquality baseClosed imageElimination Error :dependent_set_memberEquality_alt,  Error :universeIsType,  applyEquality Error :equalityIsType4,  Error :setIsType,  because_Cache Error :inhabitedIsType,  extract_by_obid Error :lambdaEquality_alt,  dependent_functionElimination axiomEquality Error :functionIsTypeImplies,  Error :functionIsType,  universeEquality Error :isect_memberEquality_alt,  isectElimination Error :isectIsTypeImplies

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    respects-equality(T;\{x:T|  P[x]\}  )

Date html generated: 2019_06_20-AM-11_13_42
Last ObjectModification: 2018_11_28-AM-11_09_49

Theory : core_2

Home Index