Description: Obsolete version of ensn1 as of 23-Sep-2024. (Contributed by NM, 4-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ensn1OLD.1 | |- A e. _V |
|
| Assertion | ensn1OLD | |- { A } ~~ 1o |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ensn1OLD.1 | |- A e. _V |
|
| 2 | snex | |- { <. A , (/) >. } e. _V |
|
| 3 | f1oeq1 | |- ( f = { <. A , (/) >. } -> ( f : { A } -1-1-onto-> { (/) } <-> { <. A , (/) >. } : { A } -1-1-onto-> { (/) } ) ) |
|
| 4 | 0ex | |- (/) e. _V |
|
| 5 | 1 4 | f1osn | |- { <. A , (/) >. } : { A } -1-1-onto-> { (/) } |
| 6 | 2 3 5 | ceqsexv2d | |- E. f f : { A } -1-1-onto-> { (/) } |
| 7 | bren | |- ( { A } ~~ { (/) } <-> E. f f : { A } -1-1-onto-> { (/) } ) |
|
| 8 | 6 7 | mpbir | |- { A } ~~ { (/) } |
| 9 | df1o2 | |- 1o = { (/) } |
|
| 10 | 8 9 | breqtrri | |- { A } ~~ 1o |