This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralf0

Description: The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005) (Proof shortened by JJ, 14-Jul-2021)

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

Proof

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