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

Metamath Proof Explorer

Theorem reu3

Description: A way to express restricted uniqueness. (Contributed by NM, 24-Oct-2006)

Ref Expression
Assertion reu3 ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 reurex ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 )
2 reu6 ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
3 biimp ⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝜑 → 𝑥 = 𝑦 ) )
4 3 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
5 4 reximi ⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
6 2 5 sylbi ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
7 1 6 jca ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
8 rexex ⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) → ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
9 8 anim2i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
10 eu3v ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) ) )
11 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
12 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
13 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
14 impexp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
15 14 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
16 13 15 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
17 16 exbii ⊢ ( ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
18 12 17 anbi12i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) ) )
19 10 11 18 3bitr4i ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
20 9 19 sylibr ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )
21 7 20 impbii ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )