Description: Variant of dftr2 with commuted quantifiers, useful for shortening proofs and avoiding ax-11 . (Contributed by BTernaryTau, 28-Dec-2024)