Theorem wl-dfralflem 34837

Description: Lemma for wl-dfralf 34838 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 2159	. 2 ⊢ (∀𝑦∀𝑥(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥∀𝑦(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)))
2		bi2.04 391	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑)))
3		equcom 2021	. . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
4	3	imbi1i 352	. . . . . 6 ⊢ ((𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑)) ↔ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)))
5	2, 4	bitri 277	. . . . 5 ⊢ ((𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)))
6	5	albii 1816	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)))
7		eleq1w 2895	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	imbi1d 344	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
9	8	equsalvw 2006	. . . 4 ⊢ (∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → 𝜑))
10	6, 9	bitri 277	. . 3 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → 𝜑))
11	10	albii 1816	. 2 ⊢ (∀𝑥∀𝑦(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
12	1, 11	bitri 277	1 ⊢ (∀𝑦∀𝑥(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1531   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-11 2157

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-clel 2893

This theorem is referenced by:  wl-dfralf  34838  wl-dfralv  34840