Metamath Proof Explorer

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 A y A φ
Assertion rgen2a x A y A φ


Step Hyp Ref Expression
1 rgen2a.1 x A y A φ
2 eleq1 z = x z A x A
3 2 dvelimv ¬ y y = x x A y x A
4 1 ex x A y A φ
5 4 alimi y x A y y A φ
6 3 5 syl6com x A ¬ y y = x y y A φ
7 eleq1 y = x y A x A
8 7 biimpd y = x y A x A
9 8 4 syli y = x y A φ
10 9 alimi y y = x y y A φ
11 6 10 pm2.61d2 x A y y A φ
12 df-ral y A φ y y A φ
13 11 12 sylibr x A y A φ
14 13 rgen x A y A φ