Theorem reu5 3378

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 2603	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3377	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3096	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3376	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 639	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1806   ∈ wcel 2149  ∃*wmo 2571  ∃!weu 2602  ∃wrex 3095  ∃!wreu 3374  ∃*wrmo 3375

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 210  df-an 401  df-eu 2603  df-rex 3096  df-rmo 3376  df-reu 3377

This theorem is referenced by:  reurmo  3379  reurex  3380  cbvreuw  3402  reueq1  3408  reueq1f  3414  reu4  3703  reueq  3709  2reu5a  3716  2reurex  3732  2rexreu  3734  reuan  3858  2reu1  3859  reusv1  5369  wereu  5658  wereu2  5659  fncnv  6610  moriotass  7400  supeu  9413  infeu  9457  ttrcltr  9684  resqreu  15302  sqrtneg  15317  sqreu  15411  catideu  17730  poslubd  18466  ismgmid  18722  mndideu  18802  frlmup4  21919  evlseu  22202  ply1divalg  26263  2sqreulem1  27575  2sqreunnlem1  27578  nosupno  27832  nosupbday  27834  nosupbnd1  27843  nosupbnd2  27845  noinfno  27847  noinfbday  27849  noinfbnd1  27858  noinfbnd2  27860  noreceuw  28349  tglinethrueu  28873  foot  28960  mideu  28977  prlngeu  29157  nbusgredgeu  29656  pjhtheu  31686  pjpreeq  31690  cnlnadjeui  32369  cvmliftlem14  35687  cvmlift2lem13  35705  cvmlift3  35718  r1peuqusdeg1  36033  linethrueu  36546  phpreu  38142  poimirlem18  38176  poimirlem21  38179  raldmqsmo  38901  disjimdmqseq  39347  primrootsunit1  42753  addinvcom  43082  reutruALT  49467  lubeldm2  49618  glbeldm2  49619  upeu  49833