Theorem reu5 3344

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 3343	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3062	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3342	. . 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 2537  ∃!weu 2568  ∃wrex 3061  ∃!wreu 3340  ∃*wrmo 3341

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 3062  df-rmo 3342  df-reu 3343

This theorem is referenced by:  reurmo  3345  reurex  3346  cbvreuw  3368  reueq1  3374  reueq1f  3380  reu4  3677  reueq  3683  2reu5a  3690  2reurex  3706  2rexreu  3708  reuan  3834  2reu1  3835  reusv1  5339  wereu  5627  wereu2  5628  fncnv  6571  moriotass  7356  supeu  9367  infeu  9411  ttrcltr  9637  resqreu  15214  sqrtneg  15229  sqreu  15323  catideu  17641  poslubd  18377  ismgmid  18633  mndideu  18713  frlmup4  21781  evlseu  22061  ply1divalg  26103  2sqreulem1  27409  2sqreunnlem1  27412  nosupno  27667  nosupbday  27669  nosupbnd1  27678  nosupbnd2  27680  noinfno  27682  noinfbday  27684  noinfbnd1  27693  noinfbnd2  27695  noreceuw  28183  tglinethrueu  28707  foot  28790  mideu  28806  nbusgredgeu  29435  pjhtheu  31465  pjpreeq  31469  cnlnadjeui  32148  cvmliftlem14  35479  cvmlift2lem13  35497  cvmlift3  35510  r1peuqusdeg1  35825  linethrueu  36338  phpreu  37925  poimirlem18  37959  poimirlem21  37962  raldmqsmo  38684  disjimdmqseq  39130  primrootsunit1  42536  addinvcom  42864  reutruALT  49280  lubeldm2  49431  glbeldm2  49432  upeu  49646