Theorem rgen2 1248

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

Hypothesis

Ref	Expression
rgen2.1	⊢ ((x ∈ A ∧ y ∈ A) → φ)

Assertion

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

Distinct variable group(s):   y,A

Proof of Theorem rgen2

Step	Hyp	Ref	Expression
1		rgen2.1	. . . . . . . 8 ⊢ ((x ∈ A ∧ y ∈ A) → φ)
2	1	exp 291	. . . . . . 7 ⊢ (x ∈ A → (y ∈ A → φ))
3	2	ax-gen 677	. . . . . 6 ⊢ ∀y(x ∈ A → (y ∈ A → φ))
4		eq5 824	. . . . . . 7 ⊢ (∀y y = x → ∀y∀y y = x)
5		eleq1 1149	. . . . . . . . 9 ⊢ (y = x → (y ∈ A ↔ x ∈ A))
6	5	a4s 682	. . . . . . . 8 ⊢ (∀y y = x → (y ∈ A ↔ x ∈ A))
7	6	imbi1d 465	. . . . . . 7 ⊢ (∀y y = x → ((y ∈ A → (y ∈ A → φ)) ↔ (x ∈ A → (y ∈ A → φ))))
8	4, 7	biald 782	. . . . . 6 ⊢ (∀y y = x → (∀y(y ∈ A → (y ∈ A → φ)) ↔ ∀y(x ∈ A → (y ∈ A → φ))))
9	3, 8	mpbiri 169	. . . . 5 ⊢ (∀y y = x → ∀y(y ∈ A → (y ∈ A → φ)))
10		pm2.43 57	. . . . . 6 ⊢ ((y ∈ A → (y ∈ A → φ)) → (y ∈ A → φ))
11	10	19.20i 691	. . . . 5 ⊢ (∀y(y ∈ A → (y ∈ A → φ)) → ∀y(y ∈ A → φ))
12		ax-1 3	. . . . 5 ⊢ (∀y(y ∈ A → φ) → (x ∈ A → ∀y(y ∈ A → φ)))
13	9, 11, 12	3syl 21	. . . 4 ⊢ (∀y y = x → (x ∈ A → ∀y(y ∈ A → φ)))
14		ax-17 925	. . . . . 6 ⊢ (z ∈ A → ∀y z ∈ A)
15		eleq1 1149	. . . . . 6 ⊢ (z = x → (z ∈ A ↔ x ∈ A))
16	14, 15	ddelim 1000	. . . . 5 ⊢ (¬ ∀y y = x → (x ∈ A → ∀y x ∈ A))
17	2	19.20i 691	. . . . 5 ⊢ (∀y x ∈ A → ∀y(y ∈ A → φ))
18	16, 17	syl6 23	. . . 4 ⊢ (¬ ∀y y = x → (x ∈ A → ∀y(y ∈ A → φ)))
19	13, 18	pm2.61i 110	. . 3 ⊢ (x ∈ A → ∀y(y ∈ A → φ))
20		df-ral 1205	. . 3 ⊢ (∀y ∈ A φ ↔ ∀y(y ∈ A → φ))
21	19, 20	sylibr 175	. 2 ⊢ (x ∈ A → ∀y ∈ A φ)
22	21	rgen 1247	1 ⊢ ∀x ∈ A ∀y ∈ A φ

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672   = weq 797   ∈ wcel 1092  ∀wral 1201

This theorem is referenced by:  rgen3 1265  itlso 2151  ordon 2238  isoid 2933  f1owe 2943  df1st2 3098  oawordeulem 3156  unfilem2 3439  aceq5lem4 3561  kmlem8 3587  alephiso 3697  negeu 4124  receu 4215  creur 4532  creui 4533  om2uzf1o 4656  climunii 4883  hlimunii 5143  hlimreu 5145  helch 5151  hsn0elch 5155  shscl 5282  shintcl 5294

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-cleq 1097  df-clel 1099  df-ral 1205

metamath.org