Theorem 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 -> ( dom R /. R ) = { t | E! u e. dom R t = [ u ] R } )

Proof

Step	Hyp	Ref	Expression
1		disjimrmoeqec	|- ( Disj R -> E* u e. dom R t = [ u ] R )
2	1	biantrud	|- ( Disj R -> ( t e. ( dom R /. R ) <-> ( t e. ( dom R /. R ) /\ E* u e. dom R t = [ u ] R ) ) )
3		elqsg	|- ( t e. _V -> ( t e. ( dom R /. R ) <-> E. u e. dom R t = [ u ] R ) )
4	3	elv	|- ( t e. ( dom R /. R ) <-> E. u e. dom R t = [ u ] R )
5	4	anbi1i	|- ( ( t e. ( dom R /. R ) /\ E* u e. dom R t = [ u ] R ) <-> ( E. u e. dom R t = [ u ] R /\ E* u e. dom R t = [ u ] R ) )
6		reu5	|- ( E! u e. dom R t = [ u ] R <-> ( E. u e. dom R t = [ u ] R /\ E* u e. dom R t = [ u ] R ) )
7	5 6	bitr4i	|- ( ( t e. ( dom R /. R ) /\ E* u e. dom R t = [ u ] R ) <-> E! u e. dom R t = [ u ] R )
8	2 7	bitrdi	|- ( Disj R -> ( t e. ( dom R /. R ) <-> E! u e. dom R t = [ u ] R ) )
9	8	eqabdv	|- ( Disj R -> ( dom R /. R ) = { t | E! u e. dom R t = [ u ] R } )