Metamath Proof Explorer

Theorem risc

Description: Obsolete theorem, use brric2 instead. The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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

isriscg

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

bianabs

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