# 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 ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)\to {\phi }$
Assertion rgen2a ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\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}↔{x}\in {A}\right)$
3 2 dvelimv ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\to \left({x}\in {A}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {A}\right)$
4 1 ex ${⊢}{x}\in {A}\to \left({y}\in {A}\to {\phi }\right)$
5 4 alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {A}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\phi }\right)$
6 3 5 syl6com ${⊢}{x}\in {A}\to \left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\phi }\right)\right)$
7 eleq1 ${⊢}{y}={x}\to \left({y}\in {A}↔{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 {y}\phantom{\rule{.4em}{0ex}}{y}={x}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\phi }\right)$
11 6 10 pm2.61d2 ${⊢}{x}\in {A}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\phi }\right)$
12 df-ral ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\phi }\right)$
13 11 12 sylibr ${⊢}{x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
14 13 rgen ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$