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 2570	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3344	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3343	. . 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 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 2570  df-rex 3063  df-rmo 3343  df-reu 3344

This theorem is referenced by:  reurmo  3346  reurex  3347  cbvreuw  3369  reueq1  3375  reueq1f  3381  reu4  3678  reueq  3684  2reu5a  3691  2reurex  3707  2rexreu  3709  reuan  3835  2reu1  3836  reusv1  5335  wereu  5621  wereu2  5622  fncnv  6566  moriotass  7350  supeu  9361  infeu  9405  ttrcltr  9631  resqreu  15208  sqrtneg  15223  sqreu  15317  catideu  17635  poslubd  18371  ismgmid  18627  mndideu  18707  frlmup4  21794  evlseu  22074  ply1divalg  26116  2sqreulem1  27426  2sqreunnlem1  27429  nosupno  27684  nosupbday  27686  nosupbnd1  27695  nosupbnd2  27697  noinfno  27699  noinfbday  27701  noinfbnd1  27710  noinfbnd2  27712  noreceuw  28200  tglinethrueu  28724  foot  28807  mideu  28823  nbusgredgeu  29452  pjhtheu  31483  pjpreeq  31487  cnlnadjeui  32166  cvmliftlem14  35498  cvmlift2lem13  35516  cvmlift3  35529  r1peuqusdeg1  35844  linethrueu  36357  phpreu  37942  poimirlem18  37976  poimirlem21  37979  raldmqsmo  38701  disjimdmqseq  39147  primrootsunit1  42553  addinvcom  42881  reutruALT  49295  lubeldm2  49446  glbeldm2  49447  upeu  49661