Description: Equivalence of ordered pair abstraction subclass and implication. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker ssopab2bw when possible. (Contributed by NM, 27-Dec-1996) (Proof shortened by Mario Carneiro, 18-Nov-2016) (New usage is discouraged.)