Theorem euelss

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

	Ref	Expression
Assertion	euelss	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) → ∃! 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵 )
2		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 ⊤ ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⊤ ) )
3		ancom	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ⊤ ) ↔ ( ⊤ ∧ 𝑥 ∈ 𝐴 ) )
4		truan	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐴 ) ↔ 𝑥 ∈ 𝐴 )
5	3 4	bitri	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ⊤ ) ↔ 𝑥 ∈ 𝐴 )
6	5	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⊤ ) ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
7	2 6	sylbbr	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ⊤ )
8		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐵 ⊤ ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⊤ ) )
9		ancom	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ⊤ ) ↔ ( ⊤ ∧ 𝑥 ∈ 𝐵 ) )
10		truan	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐵 )
11	9 10	bitri	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ⊤ ) ↔ 𝑥 ∈ 𝐵 )
12	11	eubii	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⊤ ) ↔ ∃! 𝑥 𝑥 ∈ 𝐵 )
13	8 12	sylbbr	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐵 → ∃! 𝑥 ∈ 𝐵 ⊤ )
14		reuss	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 ⊤ ∧ ∃! 𝑥 ∈ 𝐵 ⊤ ) → ∃! 𝑥 ∈ 𝐴 ⊤ )
15	1 7 13 14	syl3an	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) → ∃! 𝑥 ∈ 𝐴 ⊤ )
16		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 ⊤ ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⊤ ) )
17	15 16	sylib	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) → ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⊤ ) )
18		ancom	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ⊤ ) )
19	4 18	bitr3i	⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ⊤ ) )
20	19	eubii	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⊤ ) )
21	17 20	sylibr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) → ∃! 𝑥 𝑥 ∈ 𝐴 )