Theorem risc

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

	Ref	Expression
Assertion	risc	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RingOpsIso S ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isriscg	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) with typecode |-
2	1	bianabs	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RingOpsIso S ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RingOpsIso S ) ) ) with typecode |-