Description: Obsolete version of snex as of 6-Mar-2026. (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 19-May-2013) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | snexOLD | |- { A } e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snexg | |- ( A e. _V -> { A } e. _V ) |
|
| 2 | snprc | |- ( -. A e. _V <-> { A } = (/) ) |
|
| 3 | 2 | biimpi | |- ( -. A e. _V -> { A } = (/) ) |
| 4 | 0ex | |- (/) e. _V |
|
| 5 | 3 4 | eqeltrdi | |- ( -. A e. _V -> { A } e. _V ) |
| 6 | 1 5 | pm2.61i | |- { A } e. _V |