Nuprl Lemma : free-from-atom-pair

[a:Atom1]. ∀[X,Y:Type]. ∀[x:X]. ∀[y:Y].  (a#<x, y>:X × Y) supposing (a#y:Y and a#x:X)


Proof




Definitions occuring in Statement :  free-from-atom: a#x:T atom: Atom$n uimplies: supposing a uall: [x:A]. B[x] pair: <a, b> product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop:
Lemmas referenced :  free-from-atom_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality freeFromAtomAxiom hypothesis sqequalRule isect_memberEquality equalityTransitivity equalitySymmetry universeEquality atomnEquality freeFromAtomApplication freeFromAtomTriviality lambdaEquality independent_pairEquality

Latex:
\mforall{}[a:Atom1].  \mforall{}[X,Y:Type].  \mforall{}[x:X].  \mforall{}[y:Y].    (a\#<x,  y>:X  \mtimes{}  Y)  supposing  (a\#y:Y  and  a\#x:X)



Date html generated: 2016_05_13-PM-03_21_34
Last ObjectModification: 2015_12_26-AM-09_11_56

Theory : atom_1


Home Index