Theorem reu5 3346

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 2573	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3345	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3064	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3344	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 634	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 304	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃*wmo 2541  ∃!weu 2572  ∃wrex 3063  ∃!wreu 3342  ∃*wrmo 3343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397  df-eu 2573  df-rex 3064  df-rmo 3344  df-reu 3345

This theorem is referenced by:  reurmo  3347  reurex  3348  cbvreuw  3370  reueq1  3376  reueq1f  3382  reu4  3672  reueq  3678  2reu5a  3685  2reurex  3701  2rexreu  3703  reuan  3828  2reu1  3829  reusv1  5326  wereu  5614  wereu2  5615  fncnv  6558  moriotass  7345  supeu  9357  infeu  9401  ttrcltr  9628  resqreu  15205  sqrtneg  15220  sqreu  15314  catideu  17632  poslubd  18368  ismgmid  18624  mndideu  18704  frlmup4  21776  evlseu  22059  ply1divalg  26121  2sqreulem1  27427  2sqreunnlem1  27430  nosupno  27685  nosupbday  27687  nosupbnd1  27696  nosupbnd2  27698  noinfno  27700  noinfbday  27702  noinfbnd1  27711  noinfbnd2  27713  noreceuw  28201  tglinethrueu  28725  foot  28808  mideu  28824  nbusgredgeu  29453  pjhtheu  31483  pjpreeq  31487  cnlnadjeui  32166  cvmliftlem14  35525  cvmlift2lem13  35543  cvmlift3  35556  r1peuqusdeg1  35871  linethrueu  36384  phpreu  37971  poimirlem18  38005  poimirlem21  38008  raldmqsmo  38730  disjimdmqseq  39176  primrootsunit1  42582  addinvcom  42909  reutruALT  49295  lubeldm2  49446  glbeldm2  49447  upeu  49661