Theorem reu5 3359

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 3072	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3071	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3073	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 626	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 302	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1785   ∈ wcel 2109  ∃*wmo 2539  ∃!weu 2569  ∃wrex 3066  ∃!wreu 3067  ∃*wrmo 3068

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 206  df-an 396  df-eu 2570  df-rex 3071  df-reu 3072  df-rmo 3073

This theorem is referenced by:  reurex  3360  reurmo  3362  reu4  3669  reueq  3675  2reu5a  3682  2reurex  3698  2rexreu  3700  reuan  3833  2reu1  3834  reusv1  5323  wereu  5584  wereu2  5585  fncnv  6503  moriotass  7258  supeu  9174  infeu  9216  ttrcltr  9435  resqreu  14945  sqrtneg  14960  sqreu  15053  catideu  17365  poslubd  18112  ismgmid  18330  mndideu  18377  frlmup4  20989  evlseu  21274  ply1divalg  25283  2sqreulem1  26575  2sqreunnlem1  26578  tglinethrueu  26981  foot  27064  mideu  27080  nbusgredgeu  27714  pjhtheu  29735  pjpreeq  29739  cnlnadjeui  30418  cvmliftlem14  33238  cvmlift2lem13  33256  cvmlift3  33269  nosupno  33885  nosupbday  33887  nosupbnd1  33896  nosupbnd2  33898  noinfno  33900  noinfbday  33902  noinfbnd1  33911  noinfbnd2  33913  linethrueu  34437  phpreu  35740  poimirlem18  35774  poimirlem21  35777  addinvcom  40393  reutruALT  46104  lubeldm2  46202  glbeldm2  46203