Theorem rgen2a 2681

Description: Generalization rule for restricted quantification. Note that x and y needn't be distinct (and illustrates the use of dvelim 2016). (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification 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		eleq1 2413	. . . . . . . 8 |- (y = x -> (y e. A <-> x e. A))
2		rgen2a.1	. . . . . . . . 9 |- ((x e. A /\ y e. A) -> ph)
3	2	ex 423	. . . . . . . 8 |- (x e. A -> (y e. A -> ph))
4	1, 3	syl6bi 219	. . . . . . 7 |- (y = x -> (y e. A -> (y e. A -> ph)))
5	4	pm2.43d 44	. . . . . 6 |- (y = x -> (y e. A -> ph))
6	5	alimi 1559	. . . . 5 |- (A.y y = x -> A.y(y e. A -> ph))
7	6	a1d 22	. . . 4 |- (A.y y = x -> (x e. A -> A.y(y e. A -> ph)))
8		eleq1 2413	. . . . . 6 |- (z = x -> (z e. A <-> x e. A))
9	8	dvelimv 1939	. . . . 5 |- (-. A.y y = x -> (x e. A -> A.y x e. A))
10	3	alimi 1559	. . . . 5 |- (A.y x e. A -> A.y(y e. A -> ph))
11	9, 10	syl6 29	. . . 4 |- (-. A.y y = x -> (x e. A -> A.y(y e. A -> ph)))
12	7, 11	pm2.61i 156	. . 3 |- (x e. A -> A.y(y e. A -> ph))
13		df-ral 2620	. . 3 |- (A.y e. A ph <-> A.y(y e. A -> ph))
14	12, 13	sylibr 203	. 2 |- (x e. A -> A.y e. A ph)
15	14	rgen 2680	1 |- A.x e. A A.y e. A ph

Syntax hints:  -. wn 3   -> wi 4   /\ wa 358  A.wal 1540   = wceq 1642   e. wcel 1710  A.wral 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-cleq 2346  df-clel 2349  df-ral 2620

This theorem is referenced by:  vfinnc  4472  ncfinraise  4482  isoid  5491  pw1fnf1o  5856  fce  6189