### Nuprl Lemma : respects-equality-set

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

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

Date html generated: 2019_06_20-AM-11_13_44
Last ObjectModification: 2018_11_28-AM-11_13_17

Theory : core_2

Home Index