Description: Hao Wang's identity axiom P6 in Irving Copi,Symbolic Logic (5th ed.,
1979), p. 328. In traditional predicate calculus, this is a sole axiom
for identity from which the usual ones can be derived. Usage of this
theorem is discouraged because it depends on ax-13 . (Contributed by NM, 9-May-2005)(Revised by Mario Carneiro, 6-Oct-2016)(New usage is discouraged.)