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 ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) → ∃! 𝑥 𝑥 ∈ 𝐴 )

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 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) → ∃! 𝑥 𝑥 ∈ 𝐴 )