Description: Remove hypothesis from grur1 . Illustration of how to remove a "definitional hypothesis". This makes its uses longer, but the theorem feels more self-contained. It looks preferable when the defined term appears only once in the conclusion. (Contributed by BJ, 14-Sep-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-grur1 | |- ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> U = ( R1 ` ( U i^i On ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- ( U i^i On ) = ( U i^i On ) |
|
| 2 | 1 | grur1 | |- ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> U = ( R1 ` ( U i^i On ) ) ) |