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	⊢ ≃𝑟 = { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingIso 𝑠 ) ) }

Proof

Step	Hyp	Ref	Expression
1		isbrric2	⊢ ( 𝑟 ≃𝑟 𝑠 ↔ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingIso 𝑠 ) ) )
2	1	anbi2i	⊢ ( ( 𝑥 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑟 ≃𝑟 𝑠 ) ↔ ( 𝑥 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingIso 𝑠 ) ) ) )
3	2	2exbii	⊢ ( ∃ 𝑟 ∃ 𝑠 ( 𝑥 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑟 ≃𝑟 𝑠 ) ↔ ∃ 𝑟 ∃ 𝑠 ( 𝑥 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingIso 𝑠 ) ) ) )
4		ricrel	⊢ Rel ≃𝑟
5		elrelb	⊢ ( Rel ≃𝑟 → ( 𝑥 ∈ ≃𝑟 ↔ ∃ 𝑟 ∃ 𝑠 ( 𝑥 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑟 ≃𝑟 𝑠 ) ) )
6	4 5	ax-mp	⊢ ( 𝑥 ∈ ≃𝑟 ↔ ∃ 𝑟 ∃ 𝑠 ( 𝑥 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑟 ≃𝑟 𝑠 ) )
7		elopab	⊢ ( 𝑥 ∈ { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingIso 𝑠 ) ) } ↔ ∃ 𝑟 ∃ 𝑠 ( 𝑥 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingIso 𝑠 ) ) ) )
8	3 6 7	3bitr4i	⊢ ( 𝑥 ∈ ≃𝑟 ↔ 𝑥 ∈ { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingIso 𝑠 ) ) } )
9	8	eqriv	⊢ ≃𝑟 = { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingIso 𝑠 ) ) }