Theorem rgen2a 2489

Description: Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim 1993. Usage of rgen2 2521 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 1509	. . . . 5 |- F/ y z e. A
2		eleq1 2203	. . . . 5 |- ( z = x -> ( z e. A <-> x e. A ) )
3	1, 2	dvelimor 1994	. . . 4 |- ( A. y y = x \/ F/ y x e. A )
4		eleq1 2203	. . . . . . . . 9 |- ( y = x -> ( y e. A <-> x e. A ) )
5		rgen2a.1	. . . . . . . . . 10 |- ( ( x e. A /\ y e. A ) -> ph )
6	5	ex 114	. . . . . . . . 9 |- ( x e. A -> ( y e. A -> ph ) )
7	4, 6	syl6bi 162	. . . . . . . 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 1432	. . . . . 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 1499	. . . . . 6 |- ( F/ y x e. A -> ( x e. A -> A. y x e. A ) )
12	6	alimi 1432	. . . . . 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 706	. . . 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 2422	. . 3 |- ( A. y e. A ph <-> A. y ( y e. A -> ph ) )
17	15, 16	sylibr 133	. 2 |- ( x e. A -> A. y e. A ph )
18	17	rgen 2488	1 |- A. x e. A A. y e. A ph

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 698   A.wal 1330   = wceq 1332   F/wnf 1437   e. wcel 1481   A.wral 2417

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-cleq 2133  df-clel 2136  df-ral 2422

This theorem is referenced by:  ordsucunielexmid  4454  onintexmid  4495  isoid  5719  issmo  6193  oawordriexmid  6374  ecopover  6535  ecopoverg  6538  1domsn  6721  unfiexmid  6814  axaddf  7700  axmulf  7701  subf  7988  negiso  8737  cnref1o  9469  xaddf  9657  ioof  9784  fzof  9952  xrnegiso  11063  reeff1  11443  gcdf  11697  eucalgf  11772  qredeu  11814  qnnen  11980  strsetsid  12031  hmeofn  12510  ismeti  12554  qtopbasss  12729  tgqioo  12755  peano4nninf  13375