This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑