Theorem ralidm

Description: Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997) Reduce axiom usage. (Revised by GG, 2-Sep-2024)

	Ref	Expression
Assertion	ralidm	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3		ax-1	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
4	3	axc4i	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
5		pm2.21	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
6		sp	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
7	5 6	ja	⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
8	7	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
9	4 8	impbii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
10	2	bicomi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )
11	10	imbi2i	⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
12	11	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
13	2 9 12	3bitrri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )
14	1 13	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )