©1992-2000 Colin Allen. Reproduction by any means strictly prohibited.
The text book says:
identity-elim Given a sentence Φ (at line m) containing a name α, and another sentence (at line n) that is an identity statement containing αand another name β, conclude a sentence that is the result of replacing at least one occurrence of α in Φ with β.
Condition: None Annotation: m,n =E
Assumption set: The union of the assumption sets at lines m and n.

1    (1) Fa    A
2    (2) a=b   A
1,2  (3) Fb    1,2 =E
1    (1) Fa & Ga  A
2    (2) b=a      A
1,2  (3) Fb & Ga  1,2 =E
1,2  (4) Fb & Gb  1,2 =E
1    (1) ∀x(Fxa → x=a)  A
2    (2) Fba              A
1    (3) Fba → b=a       1 ∀E
1,2  (4) b=a              2,3→E
1,2  (5) ∀x(Fxb → x=b)  1,4 =E
Comment. The rule of identity elimination is not regarded as valid in all contexts. For instance, if Frank believes that Mark Twain is a novelist then, even though Twain=Clemens, it does not follow that he believes Samuel Langhorne Clemens is a novelist (if, for example, he has heard the name "Twain" but never "Clemens"). For historical reasons, contexts where the rule fails, such as belief reports, are called intensional contexts in contrast to the extensional contexts provided by the ordinary predicates which the language developed in this chapter is intended to represent.