This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reuss2

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

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

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
2 df-reu 
 |-  ( E! x e. B ps <-> E! x ( x e. B /\ ps ) )
3 1 2 anbi12i 
 |-  ( ( E. x e. A ph /\ E! x e. B ps ) <-> ( E. x ( x e. A /\ ph ) /\ E! x ( x e. B /\ ps ) ) )
4 df-ral 
 |-  ( A. x e. A ( ph -> ps ) <-> A. x ( x e. A -> ( ph -> ps ) ) )
5 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
6 pm3.2 
 |-  ( x e. B -> ( ps -> ( x e. B /\ ps ) ) )
7 6 imim2d 
 |-  ( x e. B -> ( ( ph -> ps ) -> ( ph -> ( x e. B /\ ps ) ) ) )
8 5 7 syl6 
 |-  ( A C_ B -> ( x e. A -> ( ( ph -> ps ) -> ( ph -> ( x e. B /\ ps ) ) ) ) )
9 8 a2d 
 |-  ( A C_ B -> ( ( x e. A -> ( ph -> ps ) ) -> ( x e. A -> ( ph -> ( x e. B /\ ps ) ) ) ) )
10 9 imp4a 
 |-  ( A C_ B -> ( ( x e. A -> ( ph -> ps ) ) -> ( ( x e. A /\ ph ) -> ( x e. B /\ ps ) ) ) )
11 10 alimdv 
 |-  ( A C_ B -> ( A. x ( x e. A -> ( ph -> ps ) ) -> A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ps ) ) ) )
12 11 imp 
 |-  ( ( A C_ B /\ A. x ( x e. A -> ( ph -> ps ) ) ) -> A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ps ) ) )
13 4 12 sylan2b 
 |-  ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) -> A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ps ) ) )
14 euimmo 
 |-  ( A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ps ) ) -> ( E! x ( x e. B /\ ps ) -> E* x ( x e. A /\ ph ) ) )
15 13 14 syl 
 |-  ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) -> ( E! x ( x e. B /\ ps ) -> E* x ( x e. A /\ ph ) ) )
16 df-eu 
 |-  ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ E* x ( x e. A /\ ph ) ) )
17 16 simplbi2 
 |-  ( E. x ( x e. A /\ ph ) -> ( E* x ( x e. A /\ ph ) -> E! x ( x e. A /\ ph ) ) )
18 15 17 syl9 
 |-  ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) -> ( E. x ( x e. A /\ ph ) -> ( E! x ( x e. B /\ ps ) -> E! x ( x e. A /\ ph ) ) ) )
19 18 imp32 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x ( x e. A /\ ph ) /\ E! x ( x e. B /\ ps ) ) ) -> E! x ( x e. A /\ ph ) )
20 df-reu 
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
21 19 20 sylibr 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x ( x e. A /\ ph ) /\ E! x ( x e. B /\ ps ) ) ) -> E! x e. A ph )
22 3 21 sylan2b 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> E! x e. A ph )