Description: Commutation of restricted existential quantifiers. For a version based on fewer axioms see rexcom . (Contributed by Mario Carneiro, 14-Oct-2016)