Theorem rgen2a 2369

Description: Generalization rule for restricted quantification. Note that x and y needn't be distinct (and illustrates the use of dvelimor 1891). (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.)

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 1418	. . . . 5 |- F/y z e. A
2		eleq1 2097	. . . . 5 |- (z = x -> (z e. A <-> x e. A))
3	1, 2	dvelimor 1891	. . . 4 |- (A.y y = x \/ F/y x e. A)
4		eleq1 2097	. . . . . . . . 9 |- (y = x -> (y e. A <-> x e. A))
5		rgen2a.1	. . . . . . . . . 10 |- ((x e. A /\ y e. A) -> ph)
6	5	ex 108	. . . . . . . . 9 |- (x e. A -> (y e. A -> ph))
7	4, 6	syl6bi 152	. . . . . . . 8 |- (y = x -> (y e. A -> (y e. A -> ph)))
8	7	pm2.43d 44	. . . . . . 7 |- (y = x -> (y e. A -> ph))
9	8	alimi 1341	. . . . . 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 1408	. . . . . 6 |- ( F/y x e. A -> (x e. A -> A.y x e. A))
12	6	alimi 1341	. . . . . 6 |- (A.y x e. A -> A.y(y e. A -> ph))
13	11, 12	syl6 29	. . . . 5 |- ( F/y x e. A -> (x e. A -> A.y(y e. A -> ph)))
14	10, 13	jaoi 635	. . . 4 |- ((A.y y = x \/ F/y x e. A) -> (x e. A -> A.y(y e. A -> ph)))
15	3, 14	ax-mp 7	. . 3 |- (x e. A -> A.y(y e. A -> ph))
16		df-ral 2305	. . 3 |- (A.y e. A ph <-> A.y(y e. A -> ph))
17	15, 16	sylibr 137	. 2 |- (x e. A -> A.y e. A ph)
18	17	rgen 2368	1 |- A.x e. A A.y e. A ph

Syntax hints:   -> wi 4   /\ wa 97   \/ wo 628  A.wal 1240   = wceq 1242   F/wnf 1346   e. wcel 1390  A.wral 2300

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-cleq 2030  df-clel 2033  df-ral 2305

This theorem is referenced by:  ordsucunielexmid  4216  isoid  5393  issmo  5844  ecopover  6140  ecopoverg  6143  subf  7010  cnref1o  8357  ioof  8610  fzof  8771