Theorem ralidmw

Description: Idempotent law for restricted quantifier. Weak version of ralidm , which does not require ax-10 , ax-12 , but requires ax-8 . (Contributed by GG, 30-Sep-2024)

	Ref	Expression
Hypothesis	ralidmw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	ralidmw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ralidmw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3	2	imbi2i	⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
4	3	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
5		pm2.21	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
6		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
7	6 1	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → 𝜓 ) ) )
8	7	spw	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
9	5 8	ja	⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
10	9	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
11	7	hba1w	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ∀ 𝑥 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
12		ax-1	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
13	11 12	alrimih	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
14	10 13	impbii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
15	4 14	bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
16		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
17	15 16 2	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )