Theorem rgen2a 2598

Description: Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim 2073. Usage of rgen2 2630 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	|- ( ( x e. A /\ y e. A ) -> ph )

Assertion

Ref	Expression
rgen2a	|- A. x e. A A. y e. A ph

Distinct variable group:   y, A

Allowed substitution hints:   ph( x, y)   A( x)

Proof of Theorem rgen2a

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1577	. . . . 5 |- F/ y z e. A
2		eleq1 2297	. . . . 5 |- ( z = x -> ( z e. A <-> x e. A ) )
3	1, 2	dvelimor 2074	. . . 4 |- ( A. y y = x \/ F/ y x e. A )
4		eleq1 2297	. . . . . . . . 9 |- ( y = x -> ( y e. A <-> x e. A ) )
5		rgen2a.1	. . . . . . . . . 10 |- ( ( x e. A /\ y e. A ) -> ph )
6	5	ex 115	. . . . . . . . 9 |- ( x e. A -> ( y e. A -> ph ) )
7	4, 6	biimtrdi 163	. . . . . . . 8 |- ( y = x -> ( y e. A -> ( y e. A -> ph ) ) )
8	7	pm2.43d 50	. . . . . . 7 |- ( y = x -> ( y e. A -> ph ) )
9	8	alimi 1504	. . . . . 6 |- ( A. y y = x -> A. y ( y e. A -> ph ) )
10	9	a1d 22	. . . . 5 |- ( A. y y = x -> ( x e. A -> A. y ( y e. A -> ph ) ) )
11		nfr 1567	. . . . . 6 |- ( F/ y x e. A -> ( x e. A -> A. y x e. A ) )
12	6	alimi 1504	. . . . . 6 |- ( A. y x e. A -> A. y ( y e. A -> ph ) )
13	11, 12	syl6 33	. . . . 5 |- ( F/ y x e. A -> ( x e. A -> A. y ( y e. A -> ph ) ) )
14	10, 13	jaoi 724	. . . 4 |- ( ( A. y y = x \/ F/ y x e. A ) -> ( x e. A -> A. y ( y e. A -> ph ) ) )
15	3, 14	ax-mp 5	. . 3 |- ( x e. A -> A. y ( y e. A -> ph ) )
16		df-ral 2527	. . 3 |- ( A. y e. A ph <-> A. y ( y e. A -> ph ) )
17	15, 16	sylibr 134	. 2 |- ( x e. A -> A. y e. A ph )
18	17	rgen 2597	1 |- A. x e. A A. y e. A ph

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 716   A.wal 1396   = wceq 1398   F/wnf 1509   e. wcel 2205   A.wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2227  df-clel 2230  df-ral 2527

This theorem is referenced by:  ordsucunielexmid  4655  onintexmid  4697  isoid  5985  issmo  6521  oawordriexmid  6705  ecopover  6869  ecopoverg  6872  1domsn  7070  unfiexmid  7180  axaddf  8185  axmulf  8186  subf  8477  negiso  9231  cnref1o  9986  xaddf  10180  ioof  10307  fzof  10482  xrnegiso  11951  reeff1  12390  gcdf  12672  eucalgf  12756  qredeu  12798  qnnen  13199  strsetsid  13262  hmeofn  15184  ismeti  15228  qtopbasss  15403  tgqioo  15437  peano4nninf  16801