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 )