Theorem rgen2a

Description: Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim . This theorem relies on the full set of axioms up to ax-ext and it should no longer be used. Usage of rgen2 is highly encouraged. (Contributed by NM, 23-Nov-1994) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 1-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rgen2a.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝜑 )
Assertion	rgen2a	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑

Proof

Step	Hyp	Ref	Expression
1		rgen2a.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝜑 )
2		eleq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
3	2	dvelimv	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝑥 ∈ 𝐴 ) )
4	1	ex	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐴 → 𝜑 ) )
5	4	alimi	⊢ ( ∀ 𝑦 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) )
6	3 5	syl6com	⊢ ( 𝑥 ∈ 𝐴 → ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) ) )
7		eleq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
8	7	biimpd	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) )
9	8 4	syli	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 → 𝜑 ) )
10	9	alimi	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) )
11	6 10	pm2.61d2	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) )
12		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) )
13	11 12	sylibr	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 𝜑 )
14	13	rgen	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑