### Nuprl Lemma : member-nameset-diff

`∀[L,X:Cname List]. ∀[x:nameset(L)].  x ∈ nameset(L-X) supposing ¬(x ∈ X)`

Proof

Definitions occuring in Statement :  nameset: `nameset(L)` cname_deq: `CnameDeq` coordinate_name: `Cname` list-diff: `as-bs` l_member: `(x ∈ l)` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` nameset: `nameset(L)` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` cand: `A c∧ B`
Lemmas referenced :  not_wf l_member_wf coordinate_name_wf nameset_wf list_wf list-diff_wf cname_deq_wf member-list-diff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination thin setElimination rename hypothesisEquality isect_memberEquality because_Cache dependent_set_memberEquality dependent_functionElimination productElimination independent_functionElimination independent_pairFormation

Latex:
\mforall{}[L,X:Cname  List].  \mforall{}[x:nameset(L)].    x  \mmember{}  nameset(L-X)  supposing  \mneg{}(x  \mmember{}  X)

Date html generated: 2016_05_20-AM-09_28_11
Last ObjectModification: 2015_12_28-PM-04_48_35

Theory : cubical!sets

Home Index