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	|- ( E! b A R b -> A e. dom R )

Proof

Step	Hyp	Ref	Expression
1		eubrv	|- ( E! b A R b -> A e. _V )
2		iotaex	|- ( iota b A R b ) e. _V
3	2	a1i	|- ( E! b A R b -> ( iota b A R b ) e. _V )
4		iota4	|- ( E! b A R b -> [. ( iota b A R b ) / b ]. A R b )
5		sbcbr12g	|- ( ( iota b A R b ) e. _V -> ( [. ( iota b A R b ) / b ]. A R b <-> [_ ( iota b A R b ) / b ]_ A R [_ ( iota b A R b ) / b ]_ b ) )
6	2 5	ax-mp	|- ( [. ( iota b A R b ) / b ]. A R b <-> [_ ( iota b A R b ) / b ]_ A R [_ ( iota b A R b ) / b ]_ b )
7		csbconstg	|- ( ( iota b A R b ) e. _V -> [_ ( iota b A R b ) / b ]_ A = A )
8	2 7	ax-mp	|- [_ ( iota b A R b ) / b ]_ A = A
9	2	csbvargi	|- [_ ( iota b A R b ) / b ]_ b = ( iota b A R b )
10	8 9	breq12i	|- ( [_ ( iota b A R b ) / b ]_ A R [_ ( iota b A R b ) / b ]_ b <-> A R ( iota b A R b ) )
11	6 10	sylbb	|- ( [. ( iota b A R b ) / b ]. A R b -> A R ( iota b A R b ) )
12	4 11	syl	|- ( E! b A R b -> A R ( iota b A R b ) )
13		breldmg	|- ( ( A e. _V /\ ( iota b A R b ) e. _V /\ A R ( iota b A R b ) ) -> A e. dom R )
14	1 3 12 13	syl3anc	|- ( E! b A R b -> A e. dom R )