Description: Obsolete version of en1uniel as of 24-Sep-2024. (Contributed by Stefan O'Rear, 16-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | en1unielOLD | |- ( S ~~ 1o -> U. S e. S ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relen | |- Rel ~~ |
|
| 2 | 1 | brrelex1i | |- ( S ~~ 1o -> S e. _V ) |
| 3 | uniexg | |- ( S e. _V -> U. S e. _V ) |
|
| 4 | snidg | |- ( U. S e. _V -> U. S e. { U. S } ) |
|
| 5 | 2 3 4 | 3syl | |- ( S ~~ 1o -> U. S e. { U. S } ) |
| 6 | en1b | |- ( S ~~ 1o <-> S = { U. S } ) |
|
| 7 | 6 | biimpi | |- ( S ~~ 1o -> S = { U. S } ) |
| 8 | 5 7 | eleqtrrd | |- ( S ~~ 1o -> U. S e. S ) |