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, s⟩ \| ((r \in Ring \land s \in Ring) \land \exists f f \in (r RingIso s))\}$

Step	Hyp	Ref	Expression
1		isbrric2	$⊢ r ≃_{𝑟} s \leftrightarrow ((r \in Ring \land s \in Ring) \land \exists f f \in (r RingIso s))$
2	1	anbi2i	$⊢ (x = ⟨r, s⟩ \land r ≃_{𝑟} s) \leftrightarrow (x = ⟨r, s⟩ \land ((r \in Ring \land s \in Ring) \land \exists f f \in (r RingIso s)))$
3	2	2exbii	$⊢ \exists r \exists s (x = ⟨r, s⟩ \land r ≃_{𝑟} s) \leftrightarrow \exists r \exists s (x = ⟨r, s⟩ \land ((r \in Ring \land s \in Ring) \land \exists f f \in (r RingIso s)))$
4		ricrel	$⊢ Rel ≃_{𝑟}$
5		elrelb	$⊢ Rel ≃_{𝑟} \to (x \in ≃_{𝑟} \leftrightarrow \exists r \exists s (x = ⟨r, s⟩ \land r ≃_{𝑟} s))$
6	4 5	ax-mp	$⊢ x \in ≃_{𝑟} \leftrightarrow \exists r \exists s (x = ⟨r, s⟩ \land r ≃_{𝑟} s)$
7		elopab	$⊢ x \in \{⟨r, s⟩ \| ((r \in Ring \land s \in Ring) \land \exists f f \in (r RingIso s))\} \leftrightarrow \exists r \exists s (x = ⟨r, s⟩ \land ((r \in Ring \land s \in Ring) \land \exists f f \in (r RingIso s)))$
8	3 6 7	3bitr4i	$⊢ x \in ≃_{𝑟} \leftrightarrow x \in \{⟨r, s⟩ \| ((r \in Ring \land s \in Ring) \land \exists f f \in (r RingIso s))\}$
9	8	eqriv	$⊢ ≃_{𝑟} = \{⟨r, s⟩ \| ((r \in Ring \land s \in Ring) \land \exists f f \in (r RingIso s))\}$

Metamath Proof Explorer