Theorem reu5 3382

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃*wmo 2538  ∃!weu 2568  ∃wrex 3070  ∃!wreu 3378  ∃*wrmo 3379

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 2569  df-rex 3071  df-rmo 3380  df-reu 3381

This theorem is referenced by:  reurmo  3383  reurex  3384  cbvreuw  3410  reueq1  3417  reueq1f  3425  reu4  3737  reueq  3743  2reu5a  3750  2reurex  3766  2rexreu  3768  reuan  3896  2reu1  3897  reusv1  5397  wereu  5681  wereu2  5682  fncnv  6639  moriotass  7420  supeu  9494  infeu  9536  ttrcltr  9756  resqreu  15291  sqrtneg  15306  sqreu  15399  catideu  17718  poslubd  18458  ismgmid  18678  mndideu  18758  frlmup4  21821  evlseu  22107  ply1divalg  26177  2sqreulem1  27490  2sqreunnlem1  27493  nosupno  27748  nosupbday  27750  nosupbnd1  27759  nosupbnd2  27761  noinfno  27763  noinfbday  27765  noinfbnd1  27774  noinfbnd2  27776  noreceuw  28217  tglinethrueu  28647  foot  28730  mideu  28746  nbusgredgeu  29383  pjhtheu  31413  pjpreeq  31417  cnlnadjeui  32096  cvmliftlem14  35302  cvmlift2lem13  35320  cvmlift3  35333  r1peuqusdeg1  35648  linethrueu  36157  phpreu  37611  poimirlem18  37645  poimirlem21  37648  primrootsunit1  42098  addinvcom  42461  reutruALT  48725  lubeldm2  48853  glbeldm2  48854  upeu  48928