Theorem reuun2 3247

Description: Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.)

Assertion

Ref	Expression
reuun2	⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem reuun2

Step	Hyp	Ref	Expression
1		df-rex 2354	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
2		euor2 1999	. . 3 ⊢ (¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑) → (∃!𝑥((𝑥 ∈ 𝐵 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylnbi 635	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥((𝑥 ∈ 𝐵 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		df-reu 2355	. . 3 ⊢ (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑))
5		elun 3113	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
6	5	anbi1i 445	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑))
7		andir 765	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)))
8		orcom 679	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜑)))
9	7, 8	bitri 182	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐵 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜑)))
10	6, 9	bitri 182	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐵 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜑)))
11	10	eubii 1950	. . 3 ⊢ (∃!𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ∃!𝑥((𝑥 ∈ 𝐵 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜑)))
12	4, 11	bitri 182	. 2 ⊢ (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥((𝑥 ∈ 𝐵 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜑)))
13		df-reu 2355	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
14	3, 12, 13	3bitr4g 221	1 ⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 661  ∃wex 1421   ∈ wcel 1433  ∃!weu 1941  ∃wrex 2349  ∃!wreu 2350   ∪ cun 2971

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-reu 2355  df-v 2603  df-un 2977

This theorem is referenced by: (None)