Nuprl Rule : pointwiseFunctionality wrename
H x:A, J ⊢ C ext t
BY pointwiseFunctionalityWR #$i !parameter{j:l} y z vs ()
H [x:Base], [z:(x ∈ A)], J ⊢ C ext t
H x:Base, y:Base, z:(x = y ∈ A), J, !subgoal_equations(x.J; vs; x; y) ⊢ C = C[y/x] ∈ 𝕌{j}
Definitions occuring in rule :
member: t ∈ T,
base: Base,
equal: s = t ∈ T,
universe: Type,
axiom: Ax
Latex:
H x:A, J \mvdash{} C ext t
BY pointwiseFunctionalityWR \#\$i !parameter\{j:l\} y z vs ()
H [x:Base], [z:(x \mmember{} A)], J \mvdash{} C ext t
H x:Base, y:Base, z:(x = y), J, !subgoal\_equations(x.J; vs; x; y) \mvdash{} C = C[y/x]
Date html generated:
2017_09_29-PM-05_44_54
Last ObjectModification:
2015_11_25-PM-03_46_14
Theory : rules
Home
Index