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 |