Theorem ralidmOLD

Description: Obsolete version of ralidm as of 2-Sep-2024. (Contributed by NM, 28-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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