Theorem eqreu

Description: A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypothesis	eqreu.1	|- ( x = B -> ( ph <-> ps ) )
Assertion	eqreu	|- ( ( B e. A /\ ps /\ A. x e. A ( ph -> x = B ) ) -> E! x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		eqreu.1	|- ( x = B -> ( ph <-> ps ) )
2		ralbiim	|- ( A. x e. A ( ph <-> x = B ) <-> ( A. x e. A ( ph -> x = B ) /\ A. x e. A ( x = B -> ph ) ) )
3	1	ceqsralv	|- ( B e. A -> ( A. x e. A ( x = B -> ph ) <-> ps ) )
4	3	anbi2d	|- ( B e. A -> ( ( A. x e. A ( ph -> x = B ) /\ A. x e. A ( x = B -> ph ) ) <-> ( A. x e. A ( ph -> x = B ) /\ ps ) ) )
5	2 4	bitrid	|- ( B e. A -> ( A. x e. A ( ph <-> x = B ) <-> ( A. x e. A ( ph -> x = B ) /\ ps ) ) )
6		reu6i	|- ( ( B e. A /\ A. x e. A ( ph <-> x = B ) ) -> E! x e. A ph )
7	6	ex	|- ( B e. A -> ( A. x e. A ( ph <-> x = B ) -> E! x e. A ph ) )
8	5 7	sylbird	|- ( B e. A -> ( ( A. x e. A ( ph -> x = B ) /\ ps ) -> E! x e. A ph ) )
9	8	3impib	|- ( ( B e. A /\ A. x e. A ( ph -> x = B ) /\ ps ) -> E! x e. A ph )
10	9	3com23	|- ( ( B e. A /\ ps /\ A. x e. A ( ph -> x = B ) ) -> E! x e. A ph )