Description: The class of sets verifying a falsity is the empty set (closed form of abf ). (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ab0 | ⊢ ( ∀ 𝑥 ¬ 𝜑 → { 𝑥 ∣ 𝜑 } = ∅ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 | ⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) | |
| 2 | stdpc4 | ⊢ ( ∀ 𝑥 ¬ 𝜑 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) | |
| 3 | sbn | ⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑦 / 𝑥 ] 𝜑 ) | |
| 4 | 2 3 | sylib | ⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ [ 𝑦 / 𝑥 ] 𝜑 ) |
| 5 | df-clab | ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 ) | |
| 6 | 4 5 | sylnibr | ⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) |
| 7 | 1 6 | alrimih | ⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) |
| 8 | eq0 | ⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) | |
| 9 | 7 8 | sylibr | ⊢ ( ∀ 𝑥 ¬ 𝜑 → { 𝑥 ∣ 𝜑 } = ∅ ) |