Theorem rgen2a 1691

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

Hypothesis

Ref	Expression
rgen2a.1	⊢ ((x ∈ A ⋀ y ∈ A) → φ)

Assertion

Ref	Expression
rgen2a	⊢ ∀x ∈ A ∀y ∈ A φ

Distinct variable group:   y,A

Proof of Theorem rgen2a

Step	Hyp	Ref	Expression
1		rgen2a.1	. . . . . . . 8 ⊢ ((x ∈ A ⋀ y ∈ A) → φ)
2	1	ex 373	. . . . . . 7 ⊢ (x ∈ A → (y ∈ A → φ))
3	2	ax-gen 960	. . . . . 6 ⊢ ∀y(x ∈ A → (y ∈ A → φ))
4		eleq1 1526	. . . . . . . . 9 ⊢ (y = x → (y ∈ A ↔ x ∈ A))
5	4	a4s 981	. . . . . . . 8 ⊢ (∀y y = x → (y ∈ A ↔ x ∈ A))
6	5	imbi1d 611	. . . . . . 7 ⊢ (∀y y = x → ((y ∈ A → (y ∈ A → φ)) ↔ (x ∈ A → (y ∈ A → φ))))
7	6	dral2 1151	. . . . . 6 ⊢ (∀y y = x → (∀y(y ∈ A → (y ∈ A → φ)) ↔ ∀y(x ∈ A → (y ∈ A → φ))))
8	3, 7	mpbiri 194	. . . . 5 ⊢ (∀y y = x → ∀y(y ∈ A → (y ∈ A → φ)))
9		pm2.43 63	. . . . . 6 ⊢ ((y ∈ A → (y ∈ A → φ)) → (y ∈ A → φ))
10	9	19.20i 989	. . . . 5 ⊢ (∀y(y ∈ A → (y ∈ A → φ)) → ∀y(y ∈ A → φ))
11		ax-1 4	. . . . 5 ⊢ (∀y(y ∈ A → φ) → (x ∈ A → ∀y(y ∈ A → φ)))
12	8, 10, 11	3syl 20	. . . 4 ⊢ (∀y y = x → (x ∈ A → ∀y(y ∈ A → φ)))
13		ax-17 968	. . . . . 6 ⊢ (z ∈ A → ∀y z ∈ A)
14		eleq1 1526	. . . . . 6 ⊢ (z = x → (z ∈ A ↔ x ∈ A))
15	13, 14	dvelim 1347	. . . . 5 ⊢ (¬ ∀y y = x → (x ∈ A → ∀y x ∈ A))
16	2	19.20i 989	. . . . 5 ⊢ (∀y x ∈ A → ∀y(y ∈ A → φ))
17	15, 16	syl6 22	. . . 4 ⊢ (¬ ∀y y = x → (x ∈ A → ∀y(y ∈ A → φ)))
18	12, 17	pm2.61i 126	. . 3 ⊢ (x ∈ A → ∀y(y ∈ A → φ))
19		df-ral 1641	. . 3 ⊢ (∀y ∈ A φ ↔ ∀y(y ∈ A → φ))
20	18, 19	sylibr 200	. 2 ⊢ (x ∈ A → ∀y ∈ A φ)
21	20	rgen 1690	1 ⊢ ∀x ∈ A ∀y ∈ A φ

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  ∀wral 1637

This theorem is referenced by:  itlso 2854  ordon 2977  isoid 3880  f1owe 3890  df1st2 4110  df2nd2 4111  oawordeulem 4172  unfilem2 4525  abfii4 4538  aceq5lem4 4710  kmlem9 4745  alephiso 4864  axaddopr 5237  axmulopr 5238  negeu 5327  receu 5670  mulnzcnopr 5671  om2uzf1o 6238  iccf 6334  icoshftf1oi 6342  dfseq0 6495  creur 6673  creui 6674  climunii 7035  reeff1 7350  reefiso 7370  subbas 7586  sn0top 7589  fctop 7592  cctop 7594  ishausi 7724  ismsi 7740  ismeti 7741  metxp 7774  isabliOLD 8042  isabli 8043  issubgi 8059  ghgrpilem1 8070  ghgrpilem4 8073  ringsn 8100  cnph 8409  minveceu 8514  efif1 8652  circgrpOLD 8658  eff1i 8665  hhip 8965  hhph 8966  hlimunii 9029  hlimreu 9031  helch 9037  hsn0elch 9041  hhshsslem2 9058  shscl 9196  shintcl 9208  pjmf1 9578  adjvalvalt 9777  idunop 9818  idhmop 9822  0hmop 9823  adj0 9834  lnopuni 9852  lnophm 9858  riesz4 9911  cnlnadjlem9 9923  adjco 9947  pjhmop 9984  hmopidmch 9990  ghomsn 10293  cayleylem2 10317  oefil2 10441  dtt2 10462  1ded 10515

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-cleq 1462  df-clel 1465  df-ral 1641

Copyright terms: Public domain