Theorem rgen2a 1675

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 955	. . . . . 6 |- A.y(x e. A -> (y e. A -> ph))
4		eleq1 1510	. . . . . . . . 9 |- (y = x -> (y e. A <-> x e. A))
5	4	a4s 960	. . . . . . . 8 |- (A.y y = x -> (y e. A <-> x e. A))
6	5	imbi1d 611	. . . . . . 7 |- (A.y y = x -> ((y e. A -> (y e. A -> ph)) <-> (x e. A -> (y e. A -> ph))))
7	6	dral2 1138	. . . . . 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 968	. . . . 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 1190	. . . . . 6 |- (z e. A -> A.y z e. A)
14		eleq1 1510	. . . . . 6 |- (z = x -> (z e. A <-> x e. A))
15	13, 14	dvelim 1334	. . . . 5 |- (-. A.y y = x -> (x e. A -> A.y x e. A))
16	2	19.20i 968	. . . . 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 1625	. . 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 1674	1 |- A.x e. A A.y e. A ph

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 950   = wceq 1099   e. wcel 1105  A.wral 1621

This theorem is referenced by:  itlso 2827  ordon 2950  isoid 3834  f1owe 3844  df1st2 4064  df2nd2 4065  oawordeulem 4126  unfilem2 4477  abfii4 4490  aceq5lem4 4662  kmlem9 4697  alephiso 4815  axaddopr 5188  axmulopr 5189  negeu 5278  receu 5621  mulnzcnopr 5622  om2uzf1o 6189  iccf 6285  icoshftf1oi 6293  dfseq0 6446  creur 6624  creui 6625  climunii 6986  reeff1 7301  reefiso 7321  subbas 7537  sn0top 7540  fctop 7543  cctop 7545  ishausi 7672  ismsi 7688  ismeti 7689  metxp 7722  isabliOLD 7990  isabli 7991  issubgi 8007  ghgrpilem1 8018  ghgrpilem4 8021  ringsn 8048  cnph 8344  minveceu 8449  efif1 8565  circgrpOLD 8571  eff1i 8578  ghomsn 8655  cayleylem2 8677  oefil2 8791  dtt2 8812  1ded 8865  hhip 9193  hhph 9194  hlimunii 9259  hlimreu 9261  helch 9267  hsn0elch 9271  shscl 9410  shintcl 9422  pjmf1 9792  adjvalvalt 9991  idunop 10032  idhmop 10036  0hmop 10037  adj0 10048  lnopuni 10066  lnophm 10072  riesz4 10125  cnlnadjlem9 10137  adjco 10161  pjhmop 10198  hmopidmch 10204

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-cleq 1446  df-clel 1449  df-ral 1625

Copyright terms: Public domain