Description: Obsolete version of abf as of 28-Jun-2024. (Contributed by NM, 20-Jan-2012) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | abfOLD.1 | ⊢ ¬ 𝜑 | |
| Assertion | abfOLD | ⊢ { 𝑥 ∣ 𝜑 } = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abfOLD.1 | ⊢ ¬ 𝜑 | |
| 2 | ab0 | ⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ¬ 𝜑 ) | |
| 3 | 2 1 | mpgbir | ⊢ { 𝑥 ∣ 𝜑 } = ∅ |