Nuprl Rule : isect_member_caseEquality

H  ⊢ f1 = f2 ∈ B[a1/x]

  BY isect_member_caseEquality (⋂x:A. B) a1 ()
  
  H  ⊢ f1 = f2 ∈ (⋂x:A. B)
  H  ⊢ a1 = a1 ∈ A


Definitions occuring in rule :  isect: ⋂x:A. B[x],  equal: s = t ∈ T,  axiom: Ax
Latex:
H    \mvdash{}  f1  =  f2

    BY  isect\_member\_caseEquality  (\mcap{}x:A.  B)  a1  ()
   
    H    \mvdash{}  f1  =  f2
    H    \mvdash{}  a1  =  a1


Date html generated: 2017_09_29-PM-05_44_59
Last ObjectModification: 2015_11_24-PM-01_53_28

Theory : rules


Home Index