Metamath Proof Explorer

Theorem rngimrcl

Description: Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020)

Ref Expression
Assertion rngimrcl 
|- ( F e. ( R RngIsom S ) -> ( R e. _V /\ S e. _V ) )

Proof

Step Hyp Ref Expression
1 df-rngisom 
 |-  RngIsom = ( r e. _V , s e. _V |-> { f e. ( r RngHomo s ) | `' f e. ( s RngHomo r ) } )
2 1 elmpocl 
 |-  ( F e. ( R RngIsom S ) -> ( R e. _V /\ S e. _V ) )