Description: Double restricted existential quantification. For a version based on fewer axioms see r2ex . (Contributed by Mario Carneiro, 14-Oct-2016) Use r2exlem . (Revised by Wolf Lammen, 10-Jan-2020)