Metamath Proof Explorer

Theorem reuun1

Description: Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005)

Ref Expression
Assertion reuun1 
|- ( ( E. x e. A ph /\ E! x e. ( A u. B ) ( ph \/ ps ) ) -> E! x e. A ph )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  A C_ ( A u. B )
2 orc 
 |-  ( ph -> ( ph \/ ps ) )
3 2 rgenw 
 |-  A. x e. A ( ph -> ( ph \/ ps ) )
4 reuss2 
 |-  ( ( ( A C_ ( A u. B ) /\ A. x e. A ( ph -> ( ph \/ ps ) ) ) /\ ( E. x e. A ph /\ E! x e. ( A u. B ) ( ph \/ ps ) ) ) -> E! x e. A ph )
5 1 3 4 mpanl12 
 |-  ( ( E. x e. A ph /\ E! x e. ( A u. B ) ( ph \/ ps ) ) -> E! x e. A ph )