Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reu6i | Structured version Visualization version GIF version |
Description: A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Ref | Expression |
---|---|
reu6i | ⊢ ((𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝐵)) → ∃!𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2833 | . . . . 5 ⊢ (𝑦 = 𝐵 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐵)) | |
2 | 1 | bibi2d 345 | . . . 4 ⊢ (𝑦 = 𝐵 → ((𝜑 ↔ 𝑥 = 𝑦) ↔ (𝜑 ↔ 𝑥 = 𝐵))) |
3 | 2 | ralbidv 3197 | . . 3 ⊢ (𝑦 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝐵))) |
4 | 3 | rspcev 3622 | . 2 ⊢ ((𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝐵)) → ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦)) |
5 | reu6 3716 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦)) | |
6 | 4, 5 | sylibr 236 | 1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝐵)) → ∃!𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 ∃!wreu 3140 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-cleq 2814 df-clel 2893 df-ral 3143 df-rex 3144 df-reu 3145 |
This theorem is referenced by: eqreu 3719 riota5f 7141 negeu 10875 creur 11631 creui 11632 reuccatpfxs1 14108 lublecl 17598 dfod2 18690 lmieu 26569 esum2dlem 31351 fvineqsneu 34691 poimirlem16 34907 poimirlem17 34908 poimirlem19 34910 poimirlem20 34911 poimirlem22 34913 renegeulemv 39196 |
Copyright terms: Public domain | W3C validator |