### Nuprl Lemma : equiv_rel_isect2

`∀[A,B:Type].  ∀E:A ⟶ A ⟶ ℙ. (EquivRel(A;x,y.E[x;y]) `` EquivRel(A ⋂ B;x,y.E[x;y]))`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` isect2: `T1 ⋂ T2` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uimplies: `b supposing a` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  equiv_rel_subtype isect2_wf isect2_subtype_rel equiv_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination because_Cache independent_functionElimination sqequalRule lambdaEquality applyEquality functionEquality cumulativity universeEquality

Latex:
\mforall{}[A,B:Type].    \mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}.  (EquivRel(A;x,y.E[x;y])  {}\mRightarrow{}  EquivRel(A  \mcap{}  B;x,y.E[x;y]))

Date html generated: 2016_05_13-PM-04_15_03
Last ObjectModification: 2015_12_26-AM-11_30_01

Theory : rel_1

Home Index