Theorem rgen2a 2560

Description: Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim 2045. Usage of rgen2 2592 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 1551	. . . . 5 |- F/ y z e. A
2		eleq1 2268	. . . . 5 |- ( z = x -> ( z e. A <-> x e. A ) )
3	1, 2	dvelimor 2046	. . . 4 |- ( A. y y = x \/ F/ y x e. A )
4		eleq1 2268	. . . . . . . . 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 1478	. . . . . 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 1541	. . . . . 6 |- ( F/ y x e. A -> ( x e. A -> A. y x e. A ) )
12	6	alimi 1478	. . . . . 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 2489	. . 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 2559	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 1483   e. wcel 2176   A.wral 2484

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-ral 2489

This theorem is referenced by:  ordsucunielexmid  4579  onintexmid  4621  isoid  5879  issmo  6374  oawordriexmid  6556  ecopover  6720  ecopoverg  6723  1domsn  6914  unfiexmid  7015  axaddf  7981  axmulf  7982  subf  8274  negiso  9028  cnref1o  9772  xaddf  9966  ioof  10093  fzof  10266  xrnegiso  11573  reeff1  12011  gcdf  12293  eucalgf  12377  qredeu  12419  qnnen  12802  strsetsid  12865  hmeofn  14774  ismeti  14818  qtopbasss  14993  tgqioo  15027  peano4nninf  15943