Theorem reu5 3354

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 2570	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3353	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3352	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 629	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃*wmo 2538  ∃!weu 2569  ∃wrex 3062  ∃!wreu 3350  ∃*wrmo 3351

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 2570  df-rex 3063  df-rmo 3352  df-reu 3353

This theorem is referenced by:  reurmo  3355  reurex  3356  cbvreuw  3378  reueq1  3384  reueq1f  3392  reu4  3691  reueq  3697  2reu5a  3704  2reurex  3720  2rexreu  3722  reuan  3848  2reu1  3849  reusv1  5344  wereu  5628  wereu2  5629  fncnv  6573  moriotass  7357  supeu  9369  infeu  9413  ttrcltr  9637  resqreu  15187  sqrtneg  15202  sqreu  15296  catideu  17610  poslubd  18346  ismgmid  18602  mndideu  18682  frlmup4  21768  evlseu  22050  ply1divalg  26111  2sqreulem1  27425  2sqreunnlem1  27428  nosupno  27683  nosupbday  27685  nosupbnd1  27694  nosupbnd2  27696  noinfno  27698  noinfbday  27700  noinfbnd1  27709  noinfbnd2  27711  noreceuw  28199  tglinethrueu  28723  foot  28806  mideu  28822  nbusgredgeu  29451  pjhtheu  31482  pjpreeq  31486  cnlnadjeui  32165  cvmliftlem14  35513  cvmlift2lem13  35531  cvmlift3  35544  r1peuqusdeg1  35859  linethrueu  36372  phpreu  37855  poimirlem18  37889  poimirlem21  37892  raldmqsmo  38614  disjimdmqseq  39060  primrootsunit1  42467  addinvcom  42802  reutruALT  49164  lubeldm2  49315  glbeldm2  49316  upeu  49530