Theorem reu5 3345

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 2562	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3344	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3054	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3343	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 628	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃*wmo 2531  ∃!weu 2561  ∃wrex 3053  ∃!wreu 3341  ∃*wrmo 3342

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 207  df-an 396  df-eu 2562  df-rex 3054  df-rmo 3343  df-reu 3344

This theorem is referenced by:  reurmo  3346  reurex  3347  cbvreuw  3371  reueq1  3377  reueq1f  3385  reu4  3691  reueq  3697  2reu5a  3704  2reurex  3720  2rexreu  3722  reuan  3848  2reu1  3849  reusv1  5336  wereu  5615  wereu2  5616  fncnv  6555  moriotass  7338  supeu  9344  infeu  9388  ttrcltr  9612  resqreu  15159  sqrtneg  15174  sqreu  15268  catideu  17581  poslubd  18317  ismgmid  18539  mndideu  18619  frlmup4  21708  evlseu  21988  ply1divalg  26041  2sqreulem1  27355  2sqreunnlem1  27358  nosupno  27613  nosupbday  27615  nosupbnd1  27624  nosupbnd2  27626  noinfno  27628  noinfbday  27630  noinfbnd1  27639  noinfbnd2  27641  noreceuw  28099  tglinethrueu  28584  foot  28667  mideu  28683  nbusgredgeu  29311  pjhtheu  31338  pjpreeq  31342  cnlnadjeui  32021  cvmliftlem14  35270  cvmlift2lem13  35288  cvmlift3  35301  r1peuqusdeg1  35616  linethrueu  36130  phpreu  37584  poimirlem18  37618  poimirlem21  37621  primrootsunit1  42070  addinvcom  42405  reutruALT  48789  lubeldm2  48940  glbeldm2  48941  upeu  49156