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	⊢ ( ∃! 𝑏 𝐴 𝑅 𝑏 → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		brprcneu	⊢ ( ¬ 𝐴 ∈ V → ¬ ∃! 𝑏 𝐴 𝑅 𝑏 )
2	1	con4i	⊢ ( ∃! 𝑏 𝐴 𝑅 𝑏 → 𝐴 ∈ V )