Theorem raldmqseu

Description: Equivalence between "exactly one" on the quotient carrier and "at most one" globally. Provides a type-safe way to talk about unique representatives either as E! on the intended carrier or as a global E* statement. (Contributed by Peter Mazsa, 6-Feb-2026)

	Ref	Expression
Assertion	raldmqseu	⊢ ( 𝑅 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		raldmqsmo	⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
2		ralrmo3	⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
3	1 2	bitr3i	⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
4		eqelb	⊢ ( ( 𝑢 = [ 𝑡 ] 𝑅 ∧ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ) ↔ ( 𝑢 = [ 𝑡 ] 𝑅 ∧ [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) )
5		ancom	⊢ ( ( 𝑢 = [ 𝑡 ] 𝑅 ∧ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ) ↔ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
6		ancom	⊢ ( ( 𝑢 = [ 𝑡 ] 𝑅 ∧ [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) ↔ ( [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
7	4 5 6	3bitr3i	⊢ ( ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ( [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
8		eceldmqs	⊢ ( 𝑅 ∈ 𝑉 → ( [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝑡 ∈ dom 𝑅 ) )
9	8	anbi1d	⊢ ( 𝑅 ∈ 𝑉 → ( ( [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ( 𝑡 ∈ dom 𝑅 ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ) )
10	7 9	bitrid	⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ( 𝑡 ∈ dom 𝑅 ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ) )
11	10	rmobidv	⊢ ( 𝑅 ∈ 𝑉 → ( ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ∃* 𝑡 ∈ dom 𝑅 ( 𝑡 ∈ dom 𝑅 ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ) )
12		rmoanid	⊢ ( ∃* 𝑡 ∈ dom 𝑅 ( 𝑡 ∈ dom 𝑅 ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
13	11 12	bitrdi	⊢ ( 𝑅 ∈ 𝑉 → ( ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
14	13	albidv	⊢ ( 𝑅 ∈ 𝑉 → ( ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
15	3 14	bitrid	⊢ ( 𝑅 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )