Theorem reu6dv

Description: A condition which implies existential uniqueness. (Contributed by Thierry Arnoux, 13-Oct-2025)

	Ref	Expression
Hypotheses	reu6d.1	|- ( ph -> B e. A )
	reu6d.2	|- ( ( ph /\ x e. A ) -> ( ps <-> x = B ) )
Assertion	reu6dv	|- ( ph -> E! x e. A ps )

Proof

Step	Hyp	Ref	Expression
1		reu6d.1	|- ( ph -> B e. A )
2		reu6d.2	|- ( ( ph /\ x e. A ) -> ( ps <-> x = B ) )
3	2	ralrimiva	|- ( ph -> A. x e. A ( ps <-> x = B ) )
4		reu6i	|- ( ( B e. A /\ A. x e. A ( ps <-> x = B ) ) -> E! x e. A ps )
5	1 3 4	syl2anc	|- ( ph -> E! x e. A ps )