Theorem eubrdm

Description: If there is a unique set which is related to a class, then the class is an element of the domain of the relation. (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	eubrdm	⊢ ( ∃! 𝑏 𝐴 𝑅 𝑏 → 𝐴 ∈ dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		eubrv	⊢ ( ∃! 𝑏 𝐴 𝑅 𝑏 → 𝐴 ∈ V )
2		iotaex	⊢ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) ∈ V
3	2	a1i	⊢ ( ∃! 𝑏 𝐴 𝑅 𝑏 → ( ℩ 𝑏 𝐴 𝑅 𝑏 ) ∈ V )
4		iota4	⊢ ( ∃! 𝑏 𝐴 𝑅 𝑏 → [ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ] 𝐴 𝑅 𝑏 )
5		sbcbr12g	⊢ ( ( ℩ 𝑏 𝐴 𝑅 𝑏 ) ∈ V → ( [ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ] 𝐴 𝑅 𝑏 ↔ ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝐴 𝑅 ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝑏 ) )
6	2 5	ax-mp	⊢ ( [ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ] 𝐴 𝑅 𝑏 ↔ ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝐴 𝑅 ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝑏 )
7		csbconstg	⊢ ( ( ℩ 𝑏 𝐴 𝑅 𝑏 ) ∈ V → ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝐴 = 𝐴 )
8	2 7	ax-mp	⊢ ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝐴 = 𝐴
9	2	csbvargi	⊢ ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝑏 = ( ℩ 𝑏 𝐴 𝑅 𝑏 )
10	8 9	breq12i	⊢ ( ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝐴 𝑅 ⦋ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ⦌ 𝑏 ↔ 𝐴 𝑅 ( ℩ 𝑏 𝐴 𝑅 𝑏 ) )
11	6 10	sylbb	⊢ ( [ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) / 𝑏 ] 𝐴 𝑅 𝑏 → 𝐴 𝑅 ( ℩ 𝑏 𝐴 𝑅 𝑏 ) )
12	4 11	syl	⊢ ( ∃! 𝑏 𝐴 𝑅 𝑏 → 𝐴 𝑅 ( ℩ 𝑏 𝐴 𝑅 𝑏 ) )
13		breldmg	⊢ ( ( 𝐴 ∈ V ∧ ( ℩ 𝑏 𝐴 𝑅 𝑏 ) ∈ V ∧ 𝐴 𝑅 ( ℩ 𝑏 𝐴 𝑅 𝑏 ) ) → 𝐴 ∈ dom 𝑅 )
14	1 3 12 13	syl3anc	⊢ ( ∃! 𝑏 𝐴 𝑅 𝑏 → 𝐴 ∈ dom 𝑅 )