Theorem rgen2a 2160

Description: Generalization rule for restricted quantification. Note that x and y needn't be distinct. (The proof was shortened by Andrew Salmon, 25-May-2011.)

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	. . . . . . . . 9 |- ((x e. A /\ y e. A) -> ph)
2	1	ex 402	. . . . . . . 8 |- (x e. A -> (y e. A -> ph))
3		eleq1 1957	. . . . . . . . 9 |- (y = x -> (y e. A <-> x e. A))
4	3	imbi1d 675	. . . . . . . 8 |- (y = x -> ((y e. A -> (y e. A -> ph)) <-> (x e. A -> (y e. A -> ph))))
5	2, 4	mpbiri 211	. . . . . . 7 |- (y = x -> (y e. A -> (y e. A -> ph)))
6	5	pm2.43d 79	. . . . . 6 |- (y = x -> (y e. A -> ph))
7	6	alimi 1338	. . . . 5 |- (A.y y = x -> A.y(y e. A -> ph))
8	7	a1d 15	. . . 4 |- (A.y y = x -> (x e. A -> A.y(y e. A -> ph)))
9		ax-17 1317	. . . . . 6 |- (z e. A -> A.y z e. A)
10		eleq1 1957	. . . . . 6 |- (z = x -> (z e. A <-> x e. A))
11	9, 10	dvelim 1743	. . . . 5 |- (-. A.y y = x -> (x e. A -> A.y x e. A))
12	2	alimi 1338	. . . . 5 |- (A.y x e. A -> A.y(y e. A -> ph))
13	11, 12	syl6 25	. . . 4 |- (-. A.y y = x -> (x e. A -> A.y(y e. A -> ph)))
14	8, 13	pm2.61i 140	. . 3 |- (x e. A -> A.y(y e. A -> ph))
15		df-ral 2109	. . 3 |- (A.y e. A ph <-> A.y(y e. A -> ph))
16	14, 15	sylibr 217	. 2 |- (x e. A -> A.y e. A ph)
17	16	rgen 2159	1 |- A.x e. A A.y e. A ph

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105

This theorem is referenced by:  itlso 3619  ordon 3863  isoid 4872  f1owe 4882  oawordeulem 5236  unfilem2 5642  abfii4 5654  ordtype 5691  aceq5lem4 5900  kmlem9 5935  alephiso 6040  nnacda 6088  axaddopr 6417  axmulopr 6418  negeui 6510  receui 6890  mulnzcnopr 6891  iccf 7570  icoshftf1oii 7578  om2uzf1oi 7712  om2uzisoi 7713  dfseq0 7806  creur 7992  creui 7993  climunii 8358  reeff1 8675  reefiso 8693  subbas 8914  sn0top 8917  fctop 8920  cctop 8922  ishausi 9062  ismsi 9078  ismeti 9079  metxp 9111  isabli 9414  issubgi 9431  ghgrpilem1 9441  ghgrpilem4 9444  ringideu 9470  ringsn 9490  cnph 9819  minveceu 9928  efif1 10091  eff1i 10098  oefil2 10275  hhip 10677  hhph 10678  hlimuniii 10741  hlimreui 10743  helch 10749  hsn0elch 10753  hhshsslem2 10771  shscli 10914  shintcli 10926  pjmf1 11296  adjvalval 11498  idunop 11539  idhmop 11543  0hmop 11544  adj0 11556  lnopunii 11574  lnophmi 11580  riesz4i 11633  cnlnadjlem9 11645  adjcoi 11670  pjhmopi 11717  hmopidmchi 11723  ghomsn 13631  cayleylem2 13642  soxp 13950  ununr 14769  zintdom 14787  dtt2 14951  1ded 15085  ordtypeOLD 15382  retopcon 15452  supfil 15560  bfplem10 16007  bfplem11 16008  ismrer1 16024  reparphtlem2 16064  issmo 16443  islati 16854  isopi 16910  isomli 16960  isabliNEW 17136  ringideuNEW 17146  atpsub 17233

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-cleq 1877  df-clel 1880  df-ral 2109

Copyright terms: Public domain