Description: Only the empty set has cardinality zero. (Contributed by NM, 23-Apr-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | cardeq0 | ⊢ ( 𝐴 ∈ 𝑉 → ( ( card ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ex | ⊢ ∅ ∈ V | |
2 | carden | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∅ ∈ V ) → ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) ) | |
3 | 1 2 | mpan2 | ⊢ ( 𝐴 ∈ 𝑉 → ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) ) |
4 | card0 | ⊢ ( card ‘ ∅ ) = ∅ | |
5 | 4 | eqeq2i | ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ ( card ‘ 𝐴 ) = ∅ ) |
6 | en0 | ⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ ) | |
7 | 3 5 6 | 3bitr3g | ⊢ ( 𝐴 ∈ 𝑉 → ( ( card ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) ) |