Theorem ralf0OLD

Description: Obsolete version of ralf0 as of 2-Sep-2024. (Contributed by NM, 26-Nov-2005) (Proof shortened by JJ, 14-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ralf0OLD.1	⊢ ¬ 𝜑
Assertion	ralf0OLD	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ralf0OLD.1	⊢ ¬ 𝜑
2		mtt	⊢ ( ¬ 𝜑 → ( ¬ 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
3	1 2	ax-mp	⊢ ( ¬ 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 → 𝜑 ) )
4	3	albii	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
5		eq0	⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
6		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
7	4 5 6	3bitr4ri	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅ )