Description: Alternate proof of p0ex which is quite different and longer if snexALT is expanded. (Contributed by NM, 23-Dec-1993) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | p0exALT | ⊢ { ∅ } ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snexALT | ⊢ { ∅ } ∈ V |