Theorem wl-dfralflem 34390

Description: Lemma for wl-dfralf 34391 and wl-dfralv . (Contributed by Wolf Lammen, 23-May-2023.)

Assertion

Ref	Expression
wl-dfralflem	⊢ (∀𝑦∀𝑥(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem wl-dfralflem

Step	Hyp	Ref	Expression
1		alcom 2130	. 2 ⊢ (∀𝑦∀𝑥(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥∀𝑦(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)))
2		bi2.04 389	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑)))
3		equcom 2006	. . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
4	3	imbi1i 351	. . . . . 6 ⊢ ((𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑)) ↔ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)))
5	2, 4	bitri 276	. . . . 5 ⊢ ((𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)))
6	5	albii 1805	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)))
7		eleq1w 2867	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	imbi1d 343	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
9	8	equsalvw 1991	. . . 4 ⊢ (∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → 𝜑))
10	6, 9	bitri 276	. . 3 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → 𝜑))
11	10	albii 1805	. 2 ⊢ (∀𝑥∀𝑦(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
12	1, 11	bitri 276	1 ⊢ (∀𝑦∀𝑥(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1523   ∈ wcel 2083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-11 2128

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-clel 2865

This theorem is referenced by:  wl-dfralf  34391  wl-dfralv  34393