Theorem rgen2a 2520

Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2005. Usage of rgen2 2552 instead is highly encouraged. (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.) (New usage is discouraged.)

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 1516	. . . . 5 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐴
2		eleq1 2229	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
3	1, 2	dvelimor 2006	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥 ∈ 𝐴)
4		eleq1 2229	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
5		rgen2a.1	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)
6	5	ex 114	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑))
7	4, 6	syl6bi 162	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑)))
8	7	pm2.43d 50	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑))
9	8	alimi 1443	. . . . . 6 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
10	9	a1d 22	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑥 → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
11		nfr 1506	. . . . . 6 ⊢ (Ⅎ𝑦 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴))
12	6	alimi 1443	. . . . . 6 ⊢ (∀𝑦 𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
13	11, 12	syl6 33	. . . . 5 ⊢ (Ⅎ𝑦 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
14	10, 13	jaoi 706	. . . 4 ⊢ ((∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)))
15	3, 14	ax-mp 5	. . 3 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
16		df-ral 2449	. . 3 ⊢ (∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))
17	15, 16	sylibr 133	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜑)
18	17	rgen 2519	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698  ∀wal 1341   = wceq 1343  Ⅎwnf 1448   ∈ wcel 2136  ∀wral 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-cleq 2158  df-clel 2161  df-ral 2449

This theorem is referenced by:  ordsucunielexmid  4508  onintexmid  4550  isoid  5778  issmo  6256  oawordriexmid  6438  ecopover  6599  ecopoverg  6602  1domsn  6785  unfiexmid  6883  axaddf  7809  axmulf  7810  subf  8100  negiso  8850  cnref1o  9588  xaddf  9780  ioof  9907  fzof  10079  xrnegiso  11203  reeff1  11641  gcdf  11905  eucalgf  11987  qredeu  12029  qnnen  12364  strsetsid  12427  hmeofn  12942  ismeti  12986  qtopbasss  13161  tgqioo  13187  peano4nninf  13886