Metamath Proof Explorer

Theorem risc

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

		Ref	Expression
	Assertion	risc	\|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RingOpsIso S ) ) )

Step	Hyp	Ref	Expression
1		isriscg	\|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) )
2	1	bianabs	\|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RingOpsIso S ) ) )

Step

Hyp

Ref

Expression

 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) )

 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RingOpsIso S ) ) )