Theorem eubrv

Description: If there is a unique set which is related to a class, then the class must be a set. (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	eubrv	$$⊢\exists !bARb\to A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		brprcneu	$$⊢\neg A\in \mathrm{V}\to \neg \exists !bARb$$
2	1	con4i	$$⊢\exists !bARb\to A\in \mathrm{V}$$