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	|- ( ( x e. A /\ y e. A ) -> ph )
Assertion	rgen2a	|- A. x e. A A. y e. A ph

Proof

Step	Hyp	Ref	Expression
1		rgen2a.1	|- ( ( x e. A /\ y e. A ) -> ph )
2		eleq1	|- ( z = x -> ( z e. A <-> x e. A ) )
3	2	dvelimv	|- ( -. A. y y = x -> ( x e. A -> A. y x e. A ) )
4	1	ex	|- ( x e. A -> ( y e. A -> ph ) )
5	4	alimi	|- ( A. y x e. A -> A. y ( y e. A -> ph ) )
6	3 5	syl6com	|- ( x e. A -> ( -. A. y y = x -> A. y ( y e. A -> ph ) ) )
7		eleq1	|- ( y = x -> ( y e. A <-> x e. A ) )
8	7	biimpd	|- ( y = x -> ( y e. A -> x e. A ) )
9	8 4	syli	|- ( y = x -> ( y e. A -> ph ) )
10	9	alimi	|- ( A. y y = x -> A. y ( y e. A -> ph ) )
11	6 10	pm2.61d2	|- ( x e. A -> A. y ( y e. A -> ph ) )
12		df-ral	|- ( A. y e. A ph <-> A. y ( y e. A -> ph ) )
13	11 12	sylibr	|- ( x e. A -> A. y e. A ph )
14	13	rgen	|- A. x e. A A. y e. A ph