Theorem ralidm

Description: Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997)

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

Proof

Step	Hyp	Ref	Expression
1		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 )
2		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 )
3	1 2	2thd	⊢ ( 𝐴 = ∅ → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )
4		neq0	⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
5		biimt	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
6		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
7		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝜑
8	7	19.23	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
9	6 8	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
10	5 9	syl6rbbr	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )
11	4 10	sylbi	⊢ ( ¬ 𝐴 = ∅ → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )
12	3 11	pm2.61i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )