Theorem isrisc

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

	Ref	Expression
Hypotheses	isrisc.1	$$⊢R\in \mathrm{V}$$
	isrisc.2	$$⊢S\in \mathrm{V}$$
Assertion	isrisc	Could not format assertion : No typesetting found for |- ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isrisc.1	$$⊢R\in \mathrm{V}$$
2		isrisc.2	$$⊢S\in \mathrm{V}$$
3		isriscg	Could not format ( ( R e. _V /\ S e. _V ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) : No typesetting found for |- ( ( R e. _V /\ S e. _V ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) with typecode |-
4	1 2 3	mp2an	Could not format ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) : No typesetting found for |- ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) with typecode |-