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

Metamath Proof Explorer

Theorem reusv2lem1

Description: Lemma for reusv2 . (Contributed by NM, 22-Oct-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2lem1 ⊢ A ≠ ∅ → ∃! x ∀ y ∈ A x = B ↔ ∃ x ∀ y ∈ A x = B

Proof

Step Hyp Ref Expression
1 n0 ⊢ A ≠ ∅ ↔ ∃ y y ∈ A
2 nfra1 ⊢ Ⅎ y ∀ y ∈ A x = B
3 2 nfmov ⊢ Ⅎ y ∃* x ∀ y ∈ A x = B
4 rsp ⊢ ∀ y ∈ A x = B → y ∈ A → x = B
5 4 com12 ⊢ y ∈ A → ∀ y ∈ A x = B → x = B
6 5 alrimiv ⊢ y ∈ A → ∀ x ∀ y ∈ A x = B → x = B
7 mo2icl ⊢ ∀ x ∀ y ∈ A x = B → x = B → ∃* x ∀ y ∈ A x = B
8 6 7 syl ⊢ y ∈ A → ∃* x ∀ y ∈ A x = B
9 3 8 exlimi ⊢ ∃ y y ∈ A → ∃* x ∀ y ∈ A x = B
10 1 9 sylbi ⊢ A ≠ ∅ → ∃* x ∀ y ∈ A x = B
11 df-eu ⊢ ∃! x ∀ y ∈ A x = B ↔ ∃ x ∀ y ∈ A x = B ∧ ∃* x ∀ y ∈ A x = B
12 11 rbaib ⊢ ∃* x ∀ y ∈ A x = B → ∃! x ∀ y ∈ A x = B ↔ ∃ x ∀ y ∈ A x = B
13 10 12 syl ⊢ A ≠ ∅ → ∃! x ∀ y ∈ A x = B ↔ ∃ x ∀ y ∈ A x = B