Theorem reueubd

Description: Restricted existential uniqueness is equivalent to existential uniqueness if the unique element is in the restricting class. (Contributed by AV, 4-Jan-2021)

	Ref	Expression
Hypothesis	reueubd.1	|- ( ( ph /\ ps ) -> x e. V )
Assertion	reueubd	|- ( ph -> ( E! x e. V ps <-> E! x ps ) )

Proof

Step	Hyp	Ref	Expression
1		reueubd.1	|- ( ( ph /\ ps ) -> x e. V )
2		df-reu	|- ( E! x e. V ps <-> E! x ( x e. V /\ ps ) )
3	1	ex	|- ( ph -> ( ps -> x e. V ) )
4	3	pm4.71rd	|- ( ph -> ( ps <-> ( x e. V /\ ps ) ) )
5	4	eubidv	|- ( ph -> ( E! x ps <-> E! x ( x e. V /\ ps ) ) )
6	2 5	bitr4id	|- ( ph -> ( E! x e. V ps <-> E! x ps ) )