Nuprl Rule : imageMemberEquality
This rule proved as lemma rule_image_member_equality_true in file rules/rules_image.v
 at https://github.com/vrahli/NuprlInCoq  
H  ⊢ (f a1) = (f a2) ∈ Image(A,f)
  BY imageMemberEquality ()
  
  H  ⊢ a1 = a2 ∈ A
  H  ⊢ f = f ∈ Base
Definitions occuring in rule : 
image-type: Image(T,f)
, 
apply: f a
, 
equal: s = t ∈ T
, 
base: Base
, 
axiom: Ax
Latex:
H    \mvdash{}  (f  a1)  =  (f  a2)
    BY  imageMemberEquality  ()
   
    H    \mvdash{}  a1  =  a2
    H    \mvdash{}  f  =  f
Date html generated:
2019_06_20-PM-04_11_44
Last ObjectModification:
2016_07_08-PM-03_48_57
Theory : rules
Home
Index