Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | eq0rdv.1 | ⊢ ( 𝜑 → ¬ 𝑥 ∈ 𝐴 ) | |
Assertion | eq0rdv | ⊢ ( 𝜑 → 𝐴 = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eq0rdv.1 | ⊢ ( 𝜑 → ¬ 𝑥 ∈ 𝐴 ) | |
2 | 1 | pm2.21d | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∅ ) ) |
3 | 2 | ssrdv | ⊢ ( 𝜑 → 𝐴 ⊆ ∅ ) |
4 | ss0 | ⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ ) | |
5 | 3 4 | syl | ⊢ ( 𝜑 → 𝐴 = ∅ ) |