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 ( 𝐴 ≠ ∅ → ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )

Proof

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