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

Metamath Proof Explorer

Theorem falseral0OLD

Description: Obsolete version of falseral0 as of 16-Feb-2026. (Contributed by AV, 30-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion falseral0OLD ⊢ ∀ x ¬ φ ∧ ∀ x ∈ A φ → A = ∅

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
2 19.26 ⊢ ∀ x ¬ φ ∧ x ∈ A → φ ↔ ∀ x ¬ φ ∧ ∀ x x ∈ A → φ
3 con3 ⊢ x ∈ A → φ → ¬ φ → ¬ x ∈ A
4 3 impcom ⊢ ¬ φ ∧ x ∈ A → φ → ¬ x ∈ A
5 4 alimi ⊢ ∀ x ¬ φ ∧ x ∈ A → φ → ∀ x ¬ x ∈ A
6 alnex ⊢ ∀ x ¬ x ∈ A ↔ ¬ ∃ x x ∈ A
7 5 6 sylib ⊢ ∀ x ¬ φ ∧ x ∈ A → φ → ¬ ∃ x x ∈ A
8 notnotb ⊢ A = ∅ ↔ ¬ ¬ A = ∅
9 neq0 ⊢ ¬ A = ∅ ↔ ∃ x x ∈ A
10 8 9 xchbinx ⊢ A = ∅ ↔ ¬ ∃ x x ∈ A
11 7 10 sylibr ⊢ ∀ x ¬ φ ∧ x ∈ A → φ → A = ∅
12 2 11 sylbir ⊢ ∀ x ¬ φ ∧ ∀ x x ∈ A → φ → A = ∅
13 1 12 sylan2b ⊢ ∀ x ¬ φ ∧ ∀ x ∈ A φ → A = ∅