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

Metamath Proof Explorer

Theorem euelss

Description: Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A C_ B -> A C_ B )
2 df-rex 
 |-  ( E. x e. A T. <-> E. x ( x e. A /\ T. ) )
3 ancom 
 |-  ( ( x e. A /\ T. ) <-> ( T. /\ x e. A ) )
4 truan 
 |-  ( ( T. /\ x e. A ) <-> x e. A )
5 3 4 bitri 
 |-  ( ( x e. A /\ T. ) <-> x e. A )
6 5 exbii 
 |-  ( E. x ( x e. A /\ T. ) <-> E. x x e. A )
7 2 6 sylbbr 
 |-  ( E. x x e. A -> E. x e. A T. )
8 df-reu 
 |-  ( E! x e. B T. <-> E! x ( x e. B /\ T. ) )
9 ancom 
 |-  ( ( x e. B /\ T. ) <-> ( T. /\ x e. B ) )
10 truan 
 |-  ( ( T. /\ x e. B ) <-> x e. B )
11 9 10 bitri 
 |-  ( ( x e. B /\ T. ) <-> x e. B )
12 11 eubii 
 |-  ( E! x ( x e. B /\ T. ) <-> E! x x e. B )
13 8 12 sylbbr 
 |-  ( E! x x e. B -> E! x e. B T. )
14 reuss 
 |-  ( ( A C_ B /\ E. x e. A T. /\ E! x e. B T. ) -> E! x e. A T. )
15 1 7 13 14 syl3an 
 |-  ( ( A C_ B /\ E. x x e. A /\ E! x x e. B ) -> E! x e. A T. )
16 df-reu 
 |-  ( E! x e. A T. <-> E! x ( x e. A /\ T. ) )
17 15 16 sylib 
 |-  ( ( A C_ B /\ E. x x e. A /\ E! x x e. B ) -> E! x ( x e. A /\ T. ) )
18 ancom 
 |-  ( ( T. /\ x e. A ) <-> ( x e. A /\ T. ) )
19 4 18 bitr3i 
 |-  ( x e. A <-> ( x e. A /\ T. ) )
20 19 eubii 
 |-  ( E! x x e. A <-> E! x ( x e. A /\ T. ) )
21 17 20 sylibr 
 |-  ( ( A C_ B /\ E. x x e. A /\ E! x x e. B ) -> E! x x e. A )