Theorem reu4

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994)

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

Proof

Step	Hyp	Ref	Expression
1		rmo4.1	|- ( x = y -> ( ph <-> ps ) )
2		reu5	|- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )
3	1	rmo4	|- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )
4	3	anbi2i	|- ( ( E. x e. A ph /\ E* x e. A ph ) <-> ( E. x e. A ph /\ A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
5	2 4	bitri	|- ( E! x e. A ph <-> ( E. x e. A ph /\ A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) ) )