Description: Obsolete version of 0sdomg as of 29-Nov-2024. (Contributed by NM, 23-Mar-2006) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0sdomgOLD | ⊢ ( 𝐴 ∈ 𝑉 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0domg | ⊢ ( 𝐴 ∈ 𝑉 → ∅ ≼ 𝐴 ) | |
| 2 | brsdom | ⊢ ( ∅ ≺ 𝐴 ↔ ( ∅ ≼ 𝐴 ∧ ¬ ∅ ≈ 𝐴 ) ) | |
| 3 | 2 | baib | ⊢ ( ∅ ≼ 𝐴 → ( ∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴 ) ) |
| 4 | 1 3 | syl | ⊢ ( 𝐴 ∈ 𝑉 → ( ∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴 ) ) |
| 5 | ensymb | ⊢ ( ∅ ≈ 𝐴 ↔ 𝐴 ≈ ∅ ) | |
| 6 | en0 | ⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ ) | |
| 7 | 5 6 | bitri | ⊢ ( ∅ ≈ 𝐴 ↔ 𝐴 = ∅ ) |
| 8 | 7 | necon3bbii | ⊢ ( ¬ ∅ ≈ 𝐴 ↔ 𝐴 ≠ ∅ ) |
| 9 | 4 8 | bitrdi | ⊢ ( 𝐴 ∈ 𝑉 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) ) |