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 3087	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3367	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 637	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 305	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1799   ∈ wcel 2142  ∃*wmo 2564  ∃!weu 2595  ∃wrex 3086  ∃!wreu 3365  ∃*wrmo 3366

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 209  df-an 400  df-eu 2596  df-rex 3087  df-rmo 3367  df-reu 3368

This theorem is referenced by:  reurmo  3370  reurex  3371  cbvreuw  3393  reueq1  3399  reueq1f  3405  reu4  3694  reueq  3700  2reu5a  3707  2reurex  3723  2rexreu  3725  reuan  3849  2reu1  3850  reusv1  5354  wereu  5643  wereu2  5644  fncnv  6594  moriotass  7385  supeu  9400  infeu  9444  ttrcltr  9671  resqreu  15279  sqrtneg  15294  sqreu  15388  catideu  17707  poslubd  18443  ismgmid  18699  mndideu  18779  frlmup4  21853  evlseu  22136  ply1divalg  26198  2sqreulem1  27510  2sqreunnlem1  27513  nosupno  27767  nosupbday  27769  nosupbnd1  27778  nosupbnd2  27780  noinfno  27782  noinfbday  27784  noinfbnd1  27793  noinfbnd2  27795  noreceuw  28284  tglinethrueu  28808  foot  28895  mideu  28911  nbusgredgeu  29567  pjhtheu  31597  pjpreeq  31601  cnlnadjeui  32280  cvmliftlem14  35647  cvmlift2lem13  35665  cvmlift3  35678  r1peuqusdeg1  35993  linethrueu  36506  phpreu  38103  poimirlem18  38137  poimirlem21  38140  raldmqsmo  38862  disjimdmqseq  39308  primrootsunit1  42714  addinvcom  43041  reutruALT  49426  lubeldm2  49577  glbeldm2  49578  upeu  49792