reu5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > reu5		Structured version Visualization version GIF version

Theorem reu5 3369

Description: Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)

**Assertion**
Ref	Expression
reu5	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

**Proof of Theorem reu5**
Step	Hyp	Ref	Expression
1		df-eu 2596	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3368	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3089	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3367	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 640	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 ∃wex 1812 ∈ wcel 2145 ∃*wmo 2564 ∃!weu 2595 ∃wrex 3088 ∃!wreu 3365 ∃*wrmo 3366

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This proof depends on definitions: df-bi 210 df-an 402 df-eu 2596 df-rex 3089 df-rmo 3367 df-reu 3368

This theorem is used by: reurmo 3370 reurex 3371 cbvreuw 3393 reueq1 3399 reueq1f 3405 reu4 3692 reueq 3698 2reu5a 3705 2reurex 3721 2rexreu 3723 reuan 3847 2reu1 3848 reusv1 5366 wereu 5655 wereu2 5656 fncnv 6610 moriotass 7406 supeu 9428 infeu 9472 ttrcltr 9699 resqreu 15343 sqrtneg 15358 sqreu 15452 catideu 17769 poslubd 18505 mgmideud 18759 ismgmid 18764 mndideuOLD 18854 frlmup4 22020 evlseu 22305 ply1divalg 26370 2sqreulem1 27690 2sqreunnlem1 27693 nosupno 27947 nosupbday 27949 nosupbnd1 27958 nosupbnd2 27960 noinfno 27962 noinfbday 27964 noinfbnd1 27973 noinfbnd2 27975 noreceuw 28464 tglinethrueu 28994 foot 29084 mideu 29101 prlngeu 29320 nbusgredgeu 29834 pjhtheu 31883 pjpreeq 31887 cnlnadjeui 32566 cvmliftlem14 35884 cvmlift2lem13 35902 cvmlift3 35915 r1peuqusdeg1 36230 linethrueu 36744 phpreu 38366 poimirlem18 38395 poimirlem21 38398 raldmqsmo 39119 disjimdmqseq 39565 primrootsunit1 42971 addinvcom 43315 reutruALT 49741 lubeldm2 49890 glbeldm2 49891 upeu 50105 ralsanmo 50748