Theorem rgen2a 1696

Description: Generalization rule for restricted quantification. Note that x and y needn't be distinct.

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

Proof of Theorem rgen2a

Step	Hyp	Ref	Expression
1		rgen2a.1	. . . . . . . 8 |- ((x e. A /\ y e. A) -> ph)
2	1	ex 373	. . . . . . 7 |- (x e. A -> (y e. A -> ph))
3	2	ax-gen 961	. . . . . 6 |- A.y(x e. A -> (y e. A -> ph))
4		eleq1 1531	. . . . . . . . 9 |- (y = x -> (y e. A <-> x e. A))
5	4	a4s 982	. . . . . . . 8 |- (A.y y = x -> (y e. A <-> x e. A))
6	5	imbi1d 612	. . . . . . 7 |- (A.y y = x -> ((y e. A -> (y e. A -> ph)) <-> (x e. A -> (y e. A -> ph))))
7	6	dral2 1153	. . . . . 6 |- (A.y y = x -> (A.y(y e. A -> (y e. A -> ph)) <-> A.y(x e. A -> (y e. A -> ph))))
8	3, 7	mpbiri 194	. . . . 5 |- (A.y y = x -> A.y(y e. A -> (y e. A -> ph)))
9		pm2.43 63	. . . . . 6 |- ((y e. A -> (y e. A -> ph)) -> (y e. A -> ph))
10	9	19.20i 990	. . . . 5 |- (A.y(y e. A -> (y e. A -> ph)) -> A.y(y e. A -> ph))
11		ax-1 4	. . . . 5 |- (A.y(y e. A -> ph) -> (x e. A -> A.y(y e. A -> ph)))
12	8, 10, 11	3syl 20	. . . 4 |- (A.y y = x -> (x e. A -> A.y(y e. A -> ph)))
13		ax-17 969	. . . . . 6 |- (z e. A -> A.y z e. A)
14		eleq1 1531	. . . . . 6 |- (z = x -> (z e. A <-> x e. A))
15	13, 14	dvelim 1350	. . . . 5 |- (-. A.y y = x -> (x e. A -> A.y x e. A))
16	2	19.20i 990	. . . . 5 |- (A.y x e. A -> A.y(y e. A -> ph))
17	15, 16	syl6 22	. . . 4 |- (-. A.y y = x -> (x e. A -> A.y(y e. A -> ph)))
18	12, 17	pm2.61i 126	. . 3 |- (x e. A -> A.y(y e. A -> ph))
19		df-ral 1646	. . 3 |- (A.y e. A ph <-> A.y(y e. A -> ph))
20	18, 19	sylibr 200	. 2 |- (x e. A -> A.y e. A ph)
21	20	rgen 1695	1 |- A.x e. A A.y e. A ph

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956  A.wral 1642

This theorem is referenced by:  itlso 2858  ordon 2982  isoid 3886  f1owe 3896  df1st2 4116  df2nd2 4117  oawordeulem 4178  unfilem2 4531  abfii4 4544  aceq5lem4 4718  kmlem9 4753  alephiso 4872  axaddopr 5245  axmulopr 5246  negeu 5335  receu 5678  mulnzcnopr 5679  om2uzf1o 6246  iccf 6342  icoshftf1oi 6350  dfseq0 6503  creur 6681  creui 6682  climunii 7043  reeff1 7358  reefiso 7378  subbas 7594  sn0top 7597  fctop 7600  cctop 7602  ishausi 7735  ismsi 7751  ismeti 7752  metxp 7786  isabliOLD 8057  isabli 8058  issubgi 8074  ghgrpilem1 8085  ghgrpilem4 8088  ringsn 8115  cnph 8422  minveceu 8527  efif1 8671  circgrpOLD 8677  eff1i 8683  hhip 8983  hhph 8984  hlimunii 9047  hlimreu 9049  helch 9055  hsn0elch 9059  hhshsslem2 9077  shscl 9219  shintcl 9231  pjmf1 9601  adjvalvalt 9800  idunop 9841  idhmop 9845  0hmop 9846  adj0 9857  lnopuni 9875  lnophm 9881  riesz4 9934  cnlnadjlem9 9946  adjco 9971  pjhmop 10011  hmopidmch 10017  ghomsn 10322  cayleylem2 10344  oefil2 10477  dtt2 10498  1ded 10551

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-cleq 1467  df-clel 1470  df-ral 1646

Copyright terms: Public domain