Metamath Proof Explorer

Theorem dfric2

Description: Alternate definition of the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 23-Aug-2026)

Ref Expression
Assertion dfric2 
|- ~=r = { <. r , s >. | ( ( r e. Ring /\ s e. Ring ) /\ E. f f e. ( r RingIso s ) ) }

Proof

Step Hyp Ref Expression
1 isbrric2 
 |-  ( r ~=r s <-> ( ( r e. Ring /\ s e. Ring ) /\ E. f f e. ( r RingIso s ) ) )
2 1 anbi2i 
 |-  ( ( x = <. r , s >. /\ r ~=r s ) <-> ( x = <. r , s >. /\ ( ( r e. Ring /\ s e. Ring ) /\ E. f f e. ( r RingIso s ) ) ) )
3 2 2exbii 
 |-  ( E. r E. s ( x = <. r , s >. /\ r ~=r s ) <-> E. r E. s ( x = <. r , s >. /\ ( ( r e. Ring /\ s e. Ring ) /\ E. f f e. ( r RingIso s ) ) ) )
4 ricrel 
 |-  Rel ~=r
5 elrelb 
 |-  ( Rel ~=r -> ( x e. ~=r <-> E. r E. s ( x = <. r , s >. /\ r ~=r s ) ) )
6 4 5 ax-mp 
 |-  ( x e. ~=r <-> E. r E. s ( x = <. r , s >. /\ r ~=r s ) )
7 elopab 
 |-  ( x e. { <. r , s >. | ( ( r e. Ring /\ s e. Ring ) /\ E. f f e. ( r RingIso s ) ) } <-> E. r E. s ( x = <. r , s >. /\ ( ( r e. Ring /\ s e. Ring ) /\ E. f f e. ( r RingIso s ) ) ) )
8 3 6 7 3bitr4i 
 |-  ( x e. ~=r <-> x e. { <. r , s >. | ( ( r e. Ring /\ s e. Ring ) /\ E. f f e. ( r RingIso s ) ) } )
9 8 eqriv 
 |-  ~=r = { <. r , s >. | ( ( r e. Ring /\ s e. Ring ) /\ E. f f e. ( r RingIso s ) ) }