Description: Alternate proof of eq0rdv . Shorter, but requiring df-clel , ax-8 . (Contributed by NM, 11-Jul-2014) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | eq0rdvALT.1 | |- ( ph -> -. x e. A ) |
|
| Assertion | eq0rdvALT | |- ( ph -> A = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eq0rdvALT.1 | |- ( ph -> -. x e. A ) |
|
| 2 | 1 | pm2.21d | |- ( ph -> ( x e. A -> x e. (/) ) ) |
| 3 | 2 | ssrdv | |- ( ph -> A C_ (/) ) |
| 4 | ss0 | |- ( A C_ (/) -> A = (/) ) |
|
| 5 | 3 4 | syl | |- ( ph -> A = (/) ) |