Nuprl Rule : isectElimination

f:(⋂x:A. B), J ⊢ ext !((!\y,v.t) Ax)

  BY isectElimination #$i ()
  
  f:(⋂x:A. B), J ⊢ a ∈ A
  f:(⋂x:A. B), J, y:B[a/x], v:(y f ∈ B[a/x]) ⊢ ext t



Definitions occuring in rule :  axiom: Ax isect: x:A. B[x] equal: t ∈ T

Latex:
H  f:(\mcap{}x:A.  B),  J  \mvdash{}  T  ext  !((!\mbackslash{}y,v.t)  f  Ax)

    BY  isectElimination  \#\$i  a  y  v  ()
   
    H  f:(\mcap{}x:A.  B),  J  \mvdash{}  a  =  a
    H  f:(\mcap{}x:A.  B),  J,  y:B[a/x],  v:(y  =  f)  \mvdash{}  T  ext  t



Date html generated: 2016_12_14-AM-08_53_24
Last ObjectModification: 2015_11_24-PM-01_53_28

Theory : rules


Home Index