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 3371

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 2597	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3370	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3091	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3369	. . 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 2147 ∃*wmo 2565 ∃!weu 2596 ∃wrex 3090 ∃!wreu 3367 ∃*wrmo 3368

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 2597 df-rex 3091 df-rmo 3369 df-reu 3370

This theorem is used by: reurmo 3372 reurex 3373 cbvreuw 3395 reueq1 3401 reueq1f 3407 reu4 3692 reueq 3698 2reu5a 3705 2reurex 3721 2rexreu 3723 reuan 3848 2reu1 3849 reusv1 5366 wereu 5654 wereu2 5655 fncnv 6643 moriotass 7440 supeu 9483 infeu 9527 ttrcltr 9754 resqreu 15462 sqrtneg 15477 sqreu 15572 catideu 17899 poslubd 18635 mgmideud 18889 ismgmid 18895 mndideuOLD 18985 frlmup4 22162 evlseu 22447 ply1divalg 26511 2sqreulem1 27830 2sqreunnlem1 27833 nosupno 28117 nosupbday 28119 nosupbnd1 28128 nosupbnd2 28130 noinfno 28132 noinfbday 28134 noinfbnd1 28143 noinfbnd2 28145 noreceuw 28634 tglinethrueu 29164 foot 29254 mideu 29271 prlngeu 29490 nbusgredgeu 30004 pjhtheu 32053 pjpreeq 32057 cnlnadjeui 32736 cvmliftlem14 36270 cvmlift2lem13 36288 cvmlift3 36301 r1peuqusdeg1 36616 linethrueu 37136 phpreu 38795 poimirlem18 38824 poimirlem21 38827 raldmqsmo 39561 disjimdmqseq 40007 primrootsunit1 43413 addinvcom 43749 reutruALT 50246 lubeldm2 50401 glbeldm2 50402 upeu 50618 ralsanmo 51335