Nuprl Rule : isectElimination

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

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


Definitions occuring in rule :  axiom: Ax,  isect: ⋂x:A. B[x],  equal: s = 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: 2019_06_20-PM-04_11_41
Last ObjectModification: 2015_11_24-PM-01_53_28

Theory : rules


Home Index