Theorem reu6i 3702

Description: A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.)

Assertion

Ref	Expression
reu6i	⊢ ((𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝐵)) → ∃!𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem reu6i

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2742	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐵))
2	1	bibi2d 342	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝜑 ↔ 𝑥 = 𝑦) ↔ (𝜑 ↔ 𝑥 = 𝐵)))
3	2	ralbidv 3157	. . 3 ⊢ (𝑦 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝐵)))
4	3	rspcev 3591	. 2 ⊢ ((𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝐵)) → ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦))
5		reu6 3700	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦))
6	4, 5	sylibr 234	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝐵)) → ∃!𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  ∃!wreu 3354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-reu 3357

This theorem is referenced by:  eqreu  3703  riota5f  7375  negeu  11418  creur  12187  creui  12188  reuccatpfxs1  14719  lublecl  18327  dfod2  19501  lmieu  28718  reu6dv  32409  esum2dlem  34089  fvineqsneu  37406  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  renegeulemv  42363  sn-subeu  42422  upeu2lem  49021