Theorem rgen2a

Description: Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim . This theorem relies on the full set of axioms up to ax-ext and it should no longer be used. Usage of rgen2 is highly encouraged. (Contributed by NM, 23-Nov-1994) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 1-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rgen2a.1	$$⊢\left(x\in A\wedge y\in A\right)\to \phi$$
Assertion	rgen2a	$$⊢\forall x\in A\forall y\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		rgen2a.1	$$⊢\left(x\in A\wedge y\in A\right)\to \phi$$
2		eleq1	$$⊢z=x\to \left(z\in A\leftrightarrow x\in A\right)$$
3	2	dvelimv	$$⊢\neg \forall yy=x\to \left(x\in A\to \forall yx\in A\right)$$
4	1	ex	$$⊢x\in A\to \left(y\in A\to \phi \right)$$
5	4	alimi	$$⊢\forall yx\in A\to \forall y\left(y\in A\to \phi \right)$$
6	3 5	syl6com	$$⊢x\in A\to \left(\neg \forall yy=x\to \forall y\left(y\in A\to \phi \right)\right)$$
7		eleq1	$$⊢y=x\to \left(y\in A\leftrightarrow x\in A\right)$$
8	7	biimpd	$$⊢y=x\to \left(y\in A\to x\in A\right)$$
9	8 4	syli	$$⊢y=x\to \left(y\in A\to \phi \right)$$
10	9	alimi	$$⊢\forall yy=x\to \forall y\left(y\in A\to \phi \right)$$
11	6 10	pm2.61d2	$$⊢x\in A\to \forall y\left(y\in A\to \phi \right)$$
12		df-ral	$$⊢\forall y\in A\phi \leftrightarrow \forall y\left(y\in A\to \phi \right)$$
13	11 12	sylibr	$$⊢x\in A\to \forall y\in A\phi$$
14	13	rgen	$$⊢\forall x\in A\forall y\in A\phi$$