Theorem rgen2a 2390

Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct (and illustrates the use of dvelimor 1908). (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.)

Hypothesis

Ref	Expression
rgen2a.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)

Assertion

Ref	Expression
rgen2a	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑

Distinct variable group:   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem rgen2a

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1435	. . . . 5 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐴
2		eleq1 2114	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
3	1, 2	dvelimor 1908	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥 ∈ 𝐴)
4		eleq1 2114	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
5		rgen2a.1	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)
6	5	ex 112	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑))
7	4, 6	syl6bi 156	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑)))
8	7	pm2.43d 48	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑))
9	8	alimi 1358	. . . . . 6 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
10	9	a1d 22	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑥 → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
11		nfr 1425	. . . . . 6 ⊢ (Ⅎ𝑦 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴))
12	6	alimi 1358	. . . . . 6 ⊢ (∀𝑦 𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
13	11, 12	syl6 33	. . . . 5 ⊢ (Ⅎ𝑦 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
14	10, 13	jaoi 644	. . . 4 ⊢ ((∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
15	3, 14	ax-mp 7	. . 3 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
16		df-ral 2326	. . 3 ⊢ (∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
17	15, 16	sylibr 141	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜑)
18	17	rgen 2389	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑

Syntax hints:   → wi 4   ∧ wa 101   ∨ wo 637  ∀wal 1255   = wceq 1257  Ⅎwnf 1363   ∈ wcel 1407  ∀wral 2321

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036

This theorem depends on definitions:  df-bi 114  df-nf 1364  df-sb 1660  df-cleq 2047  df-clel 2050  df-ral 2326

This theorem is referenced by:  ordsucunielexmid  4281  onintexmid  4322  isoid  5475  issmo  5931  ecopover  6232  ecopoverg  6235  subf  7246  cnref1o  8650  ioof  8911  fzof  9073