Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 brprcneu 
 |-  ( -. A e. _V -> -. E! b A R b )
2 1 con4i 
 |-  ( E! b A R b -> A e. _V )