Theorem eueq2 1915

Description: Equality has existential uniqueness (split into 2 cases).

Hypotheses

Ref	Expression
eueq2.1	⊢ A ∈ V
eueq2.2	⊢ B ∈ V

Assertion

Ref	Expression
eueq2	⊢ ∃!x((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B))

Distinct variable groups:   φ,x   x,A   x,B

Proof of Theorem eueq2

Step	Hyp	Ref	Expression
1		euorv 1398	. . . 4 ⊢ ((¬ ¬ φ ⋀ ∃!x(φ ⋀ x = A)) → ∃!x(¬ φ ⋁ (φ ⋀ x = A)))
2		negb 86	. . . 4 ⊢ (φ → ¬ ¬ φ)
3		eueq2.1	. . . . . 6 ⊢ A ∈ V
4	3	eueq1 1914	. . . . 5 ⊢ ∃!x x = A
5		euanv 1431	. . . . . 6 ⊢ (∃!x(φ ⋀ x = A) ↔ (φ ⋀ ∃!x x = A))
6	5	biimpr 152	. . . . 5 ⊢ ((φ ⋀ ∃!x x = A) → ∃!x(φ ⋀ x = A))
7	4, 6	mpan2 695	. . . 4 ⊢ (φ → ∃!x(φ ⋀ x = A))
8	1, 2, 7	sylanc 471	. . 3 ⊢ (φ → ∃!x(¬ φ ⋁ (φ ⋀ x = A)))
9	2	bianfd 737	. . . . . 6 ⊢ (φ → (¬ φ ↔ (¬ φ ⋀ x = B)))
10	9	orbi2d 613	. . . . 5 ⊢ (φ → (((φ ⋀ x = A) ⋁ ¬ φ) ↔ ((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B))))
11		orcom 246	. . . . 5 ⊢ ((¬ φ ⋁ (φ ⋀ x = A)) ↔ ((φ ⋀ x = A) ⋁ ¬ φ))
12	10, 11	syl5bb 531	. . . 4 ⊢ (φ → ((¬ φ ⋁ (φ ⋀ x = A)) ↔ ((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B))))
13	12	eubidv 1385	. . 3 ⊢ (φ → (∃!x(¬ φ ⋁ (φ ⋀ x = A)) ↔ ∃!x((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B))))
14	8, 13	mpbid 195	. 2 ⊢ (φ → ∃!x((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B)))
15		eueq2.2	. . . . . 6 ⊢ B ∈ V
16	15	eueq1 1914	. . . . 5 ⊢ ∃!x x = B
17		euanv 1431	. . . . . 6 ⊢ (∃!x(¬ φ ⋀ x = B) ↔ (¬ φ ⋀ ∃!x x = B))
18	17	biimpr 152	. . . . 5 ⊢ ((¬ φ ⋀ ∃!x x = B) → ∃!x(¬ φ ⋀ x = B))
19	16, 18	mpan2 695	. . . 4 ⊢ (¬ φ → ∃!x(¬ φ ⋀ x = B))
20		euorv 1398	. . . 4 ⊢ ((¬ φ ⋀ ∃!x(¬ φ ⋀ x = B)) → ∃!x(φ ⋁ (¬ φ ⋀ x = B)))
21	19, 20	mpdan 703	. . 3 ⊢ (¬ φ → ∃!x(φ ⋁ (¬ φ ⋀ x = B)))
22		id 59	. . . . . 6 ⊢ (¬ φ → ¬ φ)
23	22	bianfd 737	. . . . 5 ⊢ (¬ φ → (φ ↔ (φ ⋀ x = A)))
24	23	orbi1d 614	. . . 4 ⊢ (¬ φ → ((φ ⋁ (¬ φ ⋀ x = B)) ↔ ((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B))))
25	24	eubidv 1385	. . 3 ⊢ (¬ φ → (∃!x(φ ⋁ (¬ φ ⋀ x = B)) ↔ ∃!x((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B))))
26	21, 25	mpbid 195	. 2 ⊢ (¬ φ → ∃!x((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B)))
27	14, 26	pm2.61i 126	1 ⊢ ∃!x((φ ⋀ x = A) ⋁ (¬ φ ⋀ x = B))

Syntax hints:  ¬ wn 2   ⋁ wo 222   ⋀ wa 223   = wceq 955   ∈ wcel 957  ∃!weu 1379  Vcvv 1808

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809

Copyright terms: Public domain