Description: ax-2 rederived from the Tarski-Bernays axiom system. Often tb-ax1 is replaced with this theorem to make a "standard" system. This is because this theorem is easier to work with, despite it being longer. (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)