Step |
Hyp |
Ref |
Expression |
1 |
|
rngisoval.1 |
|
2 |
|
rngisoval.2 |
|
3 |
|
rngisoval.3 |
|
4 |
|
rngisoval.4 |
|
5 |
1 2 3 4
|
rngoisoval |
Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsIso S ) = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsIso S ) = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) with typecode |- |
6 |
5
|
eleq2d |
Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> F e. { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> F e. { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) ) with typecode |- |
7 |
|
f1oeq1 |
|
8 |
7
|
elrab |
Could not format ( F e. { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } <-> ( F e. ( R RingOpsHom S ) /\ F : X -1-1-onto-> Y ) ) : No typesetting found for |- ( F e. { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } <-> ( F e. ( R RingOpsHom S ) /\ F : X -1-1-onto-> Y ) ) with typecode |- |
9 |
6 8
|
bitrdi |
Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> ( F e. ( R RingOpsHom S ) /\ F : X -1-1-onto-> Y ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> ( F e. ( R RingOpsHom S ) /\ F : X -1-1-onto-> Y ) ) ) with typecode |- |