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	$$⊢\exists !bARb\to A\in \mathrm{dom}R$$

Proof

Step	Hyp	Ref	Expression
1		eubrv	$$⊢\exists !bARb\to A\in \mathrm{V}$$
2		iotaex	$$⊢\left(\iota b|ARb\right)\in \mathrm{V}$$
3	2	a1i	$$⊢\exists !bARb\to \left(\iota b|ARb\right)\in \mathrm{V}$$
4		iota4	$$⊢\exists !bARb\to \underset{\dot{}}{[}\left(\iota b|ARb\right)/b\underset{\dot{}}{]}ARb$$
5		sbcbr12g	$$⊢\left(\iota b|ARb\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(\iota b|ARb\right)/b\underset{\dot{}}{]}ARb\leftrightarrow ⦋\left(\iota b|ARb\right)/b⦌AR⦋\left(\iota b|ARb\right)/b⦌b\right)$$
6	2 5	ax-mp	$$⊢\underset{\dot{}}{[}\left(\iota b|ARb\right)/b\underset{\dot{}}{]}ARb\leftrightarrow ⦋\left(\iota b|ARb\right)/b⦌AR⦋\left(\iota b|ARb\right)/b⦌b$$
7		csbconstg	$$⊢\left(\iota b|ARb\right)\in \mathrm{V}\to ⦋\left(\iota b|ARb\right)/b⦌A=A$$
8	2 7	ax-mp	$$⊢⦋\left(\iota b|ARb\right)/b⦌A=A$$
9	2	csbvargi	$$⊢⦋\left(\iota b|ARb\right)/b⦌b=\left(\iota b|ARb\right)$$
10	8 9	breq12i	$$⊢⦋\left(\iota b|ARb\right)/b⦌AR⦋\left(\iota b|ARb\right)/b⦌b\leftrightarrow AR\left(\iota b|ARb\right)$$
11	6 10	sylbb	$$⊢\underset{\dot{}}{[}\left(\iota b|ARb\right)/b\underset{\dot{}}{]}ARb\to AR\left(\iota b|ARb\right)$$
12	4 11	syl	$$⊢\exists !bARb\to AR\left(\iota b|ARb\right)$$
13		breldmg	$$⊢\left(A\in \mathrm{V}\wedge \left(\iota b|ARb\right)\in \mathrm{V}\wedge AR\left(\iota b|ARb\right)\right)\to A\in \mathrm{dom}R$$
14	1 3 12 13	syl3anc	$$⊢\exists !bARb\to A\in \mathrm{dom}R$$