Nuprl Rule : dependent_set_memberEquality

H  ⊢ a1 a2 ∈ {x:A| B} 

  BY dependent_set_memberEquality !parameter{i:l} ()
  
  H  ⊢ a1 a2 ∈ A
  H  ⊢ B[a1/x]
  y:A ⊢ B[y/x] B[y/x] ∈ Type



Definitions occuring in rule :  set: {x:A| B[x]}  equal: t ∈ T universe: Type axiom: Ax

Latex:
H    \mvdash{}  a1  =  a2

    BY  dependent\_set\_memberEquality  !parameter\{i:l\}  y  ()
   
    H    \mvdash{}  a1  =  a2
    H    \mvdash{}  B[a1/x]
    H  y:A  \mvdash{}  B[y/x]  =  B[y/x]



Date html generated: 2016_12_14-AM-08_53_26
Last ObjectModification: 2015_11_25-PM-03_37_46

Theory : rules


Home Index