Theorem rgen2a 2681

Description: Generalization rule for restricted quantification. Note that x and y needn't be distinct (and illustrates the use of dvelim 2016). (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.

Hypothesis

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

Assertion

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

Distinct variable group:   y,A

Allowed substitution hints:   φ(x, y)   A(x)

Proof of Theorem rgen2a

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2413	. . . . . . . 8 ⊢ (y = x → (y ∈ A ↔ x ∈ A))
2		rgen2a.1	. . . . . . . . 9 ⊢ ((x ∈ A ∧ y ∈ A) → φ)
3	2	ex 423	. . . . . . . 8 ⊢ (x ∈ A → (y ∈ A → φ))
4	1, 3	syl6bi 219	. . . . . . 7 ⊢ (y = x → (y ∈ A → (y ∈ A → φ)))
5	4	pm2.43d 44	. . . . . 6 ⊢ (y = x → (y ∈ A → φ))
6	5	alimi 1559	. . . . 5 ⊢ (∀y y = x → ∀y(y ∈ A → φ))
7	6	a1d 22	. . . 4 ⊢ (∀y y = x → (x ∈ A → ∀y(y ∈ A → φ)))
8		eleq1 2413	. . . . . 6 ⊢ (z = x → (z ∈ A ↔ x ∈ A))
9	8	dvelimv 1939	. . . . 5 ⊢ (¬ ∀y y = x → (x ∈ A → ∀y x ∈ A))
10	3	alimi 1559	. . . . 5 ⊢ (∀y x ∈ A → ∀y(y ∈ A → φ))
11	9, 10	syl6 29	. . . 4 ⊢ (¬ ∀y y = x → (x ∈ A → ∀y(y ∈ A → φ)))
12	7, 11	pm2.61i 156	. . 3 ⊢ (x ∈ A → ∀y(y ∈ A → φ))
13		df-ral 2620	. . 3 ⊢ (∀y ∈ A φ ↔ ∀y(y ∈ A → φ))
14	12, 13	sylibr 203	. 2 ⊢ (x ∈ A → ∀y ∈ A φ)
15	14	rgen 2680	1 ⊢ ∀x ∈ A ∀y ∈ A φ

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 358  ∀wal 1540   = wceq 1642   ∈ wcel 1710  ∀wral 2615

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This proof depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-cleq 2346  df-clel 2349  df-ral 2620

This theorem is used by:  vfinnc  4472  ncfinraise  4482  isoid  5491  pw1fnf1o  5856  fce  6189