Theorem reuss

Description: Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999)

	Ref	Expression
Assertion	reuss	|- ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> E! x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ph -> ph )
2	1	rgenw	|- A. x e. A ( ph -> ph )
3		reuss2	|- ( ( ( A C_ B /\ A. x e. A ( ph -> ph ) ) /\ ( E. x e. A ph /\ E! x e. B ph ) ) -> E! x e. A ph )
4	2 3	mpanl2	|- ( ( A C_ B /\ ( E. x e. A ph /\ E! x e. B ph ) ) -> E! x e. A ph )
5	4	3impb	|- ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> E! x e. A ph )