Theorem eueq2

Description: Equality has existential uniqueness (split into 2 cases). (Contributed by NM, 5-Apr-1995)

	Ref	Expression
Hypotheses	eueq2.1	⊢ 𝐴 ∈ V
	eueq2.2	⊢ 𝐵 ∈ V
Assertion	eueq2	⊢ ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eueq2.1	⊢ 𝐴 ∈ V
2		eueq2.2	⊢ 𝐵 ∈ V
3		notnot	⊢ ( 𝜑 → ¬ ¬ 𝜑 )
4	1	eueqi	⊢ ∃! 𝑥 𝑥 = 𝐴
5		euanv	⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) ↔ ( 𝜑 ∧ ∃! 𝑥 𝑥 = 𝐴 ) )
6	5	biimpri	⊢ ( ( 𝜑 ∧ ∃! 𝑥 𝑥 = 𝐴 ) → ∃! 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) )
7	4 6	mpan2	⊢ ( 𝜑 → ∃! 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) )
8		euorv	⊢ ( ( ¬ ¬ 𝜑 ∧ ∃! 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) ) → ∃! 𝑥 ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
9	3 7 8	syl2anc	⊢ ( 𝜑 → ∃! 𝑥 ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
10		orcom	⊢ ( ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) ↔ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ¬ 𝜑 ) )
11	3	bianfd	⊢ ( 𝜑 → ( ¬ 𝜑 ↔ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
12	11	orbi2d	⊢ ( 𝜑 → ( ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ¬ 𝜑 ) ↔ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
13	10 12	bitrid	⊢ ( 𝜑 → ( ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) ↔ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
14	13	eubidv	⊢ ( 𝜑 → ( ∃! 𝑥 ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) ↔ ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
15	9 14	mpbid	⊢ ( 𝜑 → ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
16	2	eueqi	⊢ ∃! 𝑥 𝑥 = 𝐵
17		euanv	⊢ ( ∃! 𝑥 ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ↔ ( ¬ 𝜑 ∧ ∃! 𝑥 𝑥 = 𝐵 ) )
18	17	biimpri	⊢ ( ( ¬ 𝜑 ∧ ∃! 𝑥 𝑥 = 𝐵 ) → ∃! 𝑥 ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) )
19	16 18	mpan2	⊢ ( ¬ 𝜑 → ∃! 𝑥 ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) )
20		euorv	⊢ ( ( ¬ 𝜑 ∧ ∃! 𝑥 ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) → ∃! 𝑥 ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
21	19 20	mpdan	⊢ ( ¬ 𝜑 → ∃! 𝑥 ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
22		id	⊢ ( ¬ 𝜑 → ¬ 𝜑 )
23	22	bianfd	⊢ ( ¬ 𝜑 → ( 𝜑 ↔ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
24	23	orbi1d	⊢ ( ¬ 𝜑 → ( ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ↔ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
25	24	eubidv	⊢ ( ¬ 𝜑 → ( ∃! 𝑥 ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ↔ ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
26	21 25	mpbid	⊢ ( ¬ 𝜑 → ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
27	15 26	pm2.61i	⊢ ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) )