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