Theorem rgen2a 2562

Description: Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim 2046. Usage of rgen2 2594 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 1552	. . . . 5 |- F/ y z e. A
2		eleq1 2270	. . . . 5 |- ( z = x -> ( z e. A <-> x e. A ) )
3	1, 2	dvelimor 2047	. . . 4 |- ( A. y y = x \/ F/ y x e. A )
4		eleq1 2270	. . . . . . . . 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 1479	. . . . . 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 1542	. . . . . 6 |- ( F/ y x e. A -> ( x e. A -> A. y x e. A ) )
12	6	alimi 1479	. . . . . 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 718	. . . 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 2491	. . 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 2561	1 |- A. x e. A A. y e. A ph

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 710   A.wal 1371   = wceq 1373   F/wnf 1484   e. wcel 2178   A.wral 2486

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-cleq 2200  df-clel 2203  df-ral 2491

This theorem is referenced by:  ordsucunielexmid  4597  onintexmid  4639  isoid  5902  issmo  6397  oawordriexmid  6579  ecopover  6743  ecopoverg  6746  1domsn  6939  unfiexmid  7041  axaddf  8016  axmulf  8017  subf  8309  negiso  9063  cnref1o  9807  xaddf  10001  ioof  10128  fzof  10301  xrnegiso  11688  reeff1  12126  gcdf  12408  eucalgf  12492  qredeu  12534  qnnen  12917  strsetsid  12980  hmeofn  14889  ismeti  14933  qtopbasss  15108  tgqioo  15142  peano4nninf  16145