Theorem reu5 3350

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃*wmo 2535  ∃!weu 2566  ∃wrex 3058  ∃!wreu 3346  ∃*wrmo 3347

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 2567  df-rex 3059  df-rmo 3348  df-reu 3349

This theorem is referenced by:  reurmo  3351  reurex  3352  cbvreuw  3374  reueq1  3380  reueq1f  3388  reu4  3687  reueq  3693  2reu5a  3700  2reurex  3716  2rexreu  3718  reuan  3844  2reu1  3845  reusv1  5340  wereu  5618  wereu2  5619  fncnv  6563  moriotass  7345  supeu  9355  infeu  9399  ttrcltr  9623  resqreu  15173  sqrtneg  15188  sqreu  15282  catideu  17596  poslubd  18332  ismgmid  18588  mndideu  18668  frlmup4  21754  evlseu  22036  ply1divalg  26097  2sqreulem1  27411  2sqreunnlem1  27414  nosupno  27669  nosupbday  27671  nosupbnd1  27680  nosupbnd2  27682  noinfno  27684  noinfbday  27686  noinfbnd1  27695  noinfbnd2  27697  noreceuw  28160  tglinethrueu  28660  foot  28743  mideu  28759  nbusgredgeu  29388  pjhtheu  31418  pjpreeq  31422  cnlnadjeui  32101  cvmliftlem14  35440  cvmlift2lem13  35458  cvmlift3  35471  r1peuqusdeg1  35786  linethrueu  36299  phpreu  37744  poimirlem18  37778  poimirlem21  37781  primrootsunit1  42290  addinvcom  42629  reutruALT  48992  lubeldm2  49143  glbeldm2  49144  upeu  49358