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 𝑅 → ( dom 𝑅 / 𝑅 ) = { 𝑡 ∣ ∃! 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 } )

Proof

Step	Hyp	Ref	Expression
1		disjimrmoeqec	⊢ ( Disj 𝑅 → ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 )
2	1	biantrud	⊢ ( Disj 𝑅 → ( 𝑡 ∈ ( dom 𝑅 / 𝑅 ) ↔ ( 𝑡 ∈ ( dom 𝑅 / 𝑅 ) ∧ ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ) ) )
3		elqsg	⊢ ( 𝑡 ∈ V → ( 𝑡 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ) )
4	3	elv	⊢ ( 𝑡 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 )
5	4	anbi1i	⊢ ( ( 𝑡 ∈ ( dom 𝑅 / 𝑅 ) ∧ ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ) ↔ ( ∃ 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ∧ ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ) )
6		reu5	⊢ ( ∃! 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ↔ ( ∃ 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ∧ ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ) )
7	5 6	bitr4i	⊢ ( ( 𝑡 ∈ ( dom 𝑅 / 𝑅 ) ∧ ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ) ↔ ∃! 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 )
8	2 7	bitrdi	⊢ ( Disj 𝑅 → ( 𝑡 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃! 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ) )
9	8	eqabdv	⊢ ( Disj 𝑅 → ( dom 𝑅 / 𝑅 ) = { 𝑡 ∣ ∃! 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 } )

Metamath Proof Explorer

Theorem disjimdmqseq

Proof