disjimdmqseq

Description: Disjointness implies unique-generation of quotient blocks. Converts existence-quotient comprehension (see df-qs ) into a uniqueness-comprehension under disjointness; rewrites ( dom R /. R ) carriers as exactly the class of blocks with a unique representative. This is the "unique generator per block" content in a carrier-normal form. (Contributed by Peter Mazsa, 5-Feb-2026)

		Ref	Expression
	Assertion	disjimdmqseq	$⊢ Disj R \to dom R / R = \{t \| \exists! u \in dom R t = [u] R\}$

Proof

Step	Hyp	Ref	Expression
1		disjimrmoeqec	$⊢ Disj R \to \exists^{*} u \in dom R t = [u] R$
2	1	biantrud	$⊢ Disj R \to (t \in (dom R / R) \leftrightarrow (t \in (dom R / R) \land \exists^{*} u \in dom R t = [u] R))$
3		elqsg	$⊢ t \in V \to (t \in (dom R / R) \leftrightarrow \exists u \in dom R t = [u] R)$
4	3	elv	$⊢ t \in (dom R / R) \leftrightarrow \exists u \in dom R t = [u] R$
5	4	anbi1i	$⊢ (t \in (dom R / R) \land \exists^{} u \in dom R t = [u] R) \leftrightarrow (\exists u \in dom R t = [u] R \land \exists^{} u \in dom R t = [u] R)$
6		reu5	$⊢ \exists! u \in dom R t = [u] R \leftrightarrow (\exists u \in dom R t = [u] R \land \exists^{*} u \in dom R t = [u] R)$
7	5 6	bitr4i	$⊢ (t \in (dom R / R) \land \exists^{*} u \in dom R t = [u] R) \leftrightarrow \exists! u \in dom R t = [u] R$
8	2 7	bitrdi	$⊢ Disj R \to (t \in (dom R / R) \leftrightarrow \exists! u \in dom R t = [u] R)$
9	8	eqabdv	$⊢ Disj R \to dom R / R = \{t \| \exists! u \in dom R t = [u] R\}$

Metamath Proof Explorer

Theorem disjimdmqseq

Proof