Theorem reuun2 2281

Description: Transfer uniqueness to a smaller or larger class.

Assertion

Ref	Expression
reuun2	⊢ (¬ ∃x ∈ B φ → (∃!x ∈ (A ∪ B)φ ↔ ∃!x ∈ A φ))

Distinct variable groups:   x,A   x,B

Proof of Theorem reuun2

Step	Hyp	Ref	Expression
1		df-rex 1653	. . . 4 ⊢ (∃x ∈ B φ ↔ ∃x(x ∈ B ⋀ φ))
2	1	negbii 187	. . 3 ⊢ (¬ ∃x ∈ B φ ↔ ¬ ∃x(x ∈ B ⋀ φ))
3		euor2 1440	. . 3 ⊢ (¬ ∃x(x ∈ B ⋀ φ) → (∃!x((x ∈ B ⋀ φ) ⋁ (x ∈ A ⋀ φ)) ↔ ∃!x(x ∈ A ⋀ φ)))
4	2, 3	sylbi 199	. 2 ⊢ (¬ ∃x ∈ B φ → (∃!x((x ∈ B ⋀ φ) ⋁ (x ∈ A ⋀ φ)) ↔ ∃!x(x ∈ A ⋀ φ)))
5		df-reu 1654	. . 3 ⊢ (∃!x ∈ (A ∪ B)φ ↔ ∃!x(x ∈ (A ∪ B) ⋀ φ))
6		elun 2176	. . . . . 6 ⊢ (x ∈ (A ∪ B) ↔ (x ∈ A ⋁ x ∈ B))
7	6	anbi1i 483	. . . . 5 ⊢ ((x ∈ (A ∪ B) ⋀ φ) ↔ ((x ∈ A ⋁ x ∈ B) ⋀ φ))
8		andir 607	. . . . 5 ⊢ (((x ∈ A ⋁ x ∈ B) ⋀ φ) ↔ ((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ φ)))
9		orcom 246	. . . . 5 ⊢ (((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ φ)) ↔ ((x ∈ B ⋀ φ) ⋁ (x ∈ A ⋀ φ)))
10	7, 8, 9	3bitr 177	. . . 4 ⊢ ((x ∈ (A ∪ B) ⋀ φ) ↔ ((x ∈ B ⋀ φ) ⋁ (x ∈ A ⋀ φ)))
11	10	eubii 1389	. . 3 ⊢ (∃!x(x ∈ (A ∪ B) ⋀ φ) ↔ ∃!x((x ∈ B ⋀ φ) ⋁ (x ∈ A ⋀ φ)))
12	5, 11	bitr 173	. 2 ⊢ (∃!x ∈ (A ∪ B)φ ↔ ∃!x((x ∈ B ⋀ φ) ⋁ (x ∈ A ⋀ φ)))
13		df-reu 1654	. 2 ⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ⋀ φ))
14	4, 12, 13	3bitr4g 557	1 ⊢ (¬ ∃x ∈ B φ → (∃!x ∈ (A ∪ B)φ ↔ ∃!x ∈ A φ))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223   ∈ wcel 960  ∃wex 982  ∃!weu 1382  ∃wrex 1649  ∃!wreu 1650   ∪ cun 2048

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-rex 1653  df-reu 1654  df-v 1815  df-un 2053

Copyright terms: Public domain