Theorem reu5 3348

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2111  ∃*wmo 2533  ∃!weu 2563  ∃wrex 3056  ∃!wreu 3344  ∃*wrmo 3345

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 2564  df-rex 3057  df-rmo 3346  df-reu 3347

This theorem is referenced by:  reurmo  3349  reurex  3350  cbvreuw  3372  reueq1  3378  reueq1f  3386  reu4  3685  reueq  3691  2reu5a  3698  2reurex  3714  2rexreu  3716  reuan  3842  2reu1  3843  reusv1  5333  wereu  5610  wereu2  5611  fncnv  6554  moriotass  7335  supeu  9338  infeu  9382  ttrcltr  9606  resqreu  15159  sqrtneg  15174  sqreu  15268  catideu  17581  poslubd  18317  ismgmid  18573  mndideu  18653  frlmup4  21738  evlseu  22018  ply1divalg  26070  2sqreulem1  27384  2sqreunnlem1  27387  nosupno  27642  nosupbday  27644  nosupbnd1  27653  nosupbnd2  27655  noinfno  27657  noinfbday  27659  noinfbnd1  27668  noinfbnd2  27670  noreceuw  28130  tglinethrueu  28617  foot  28700  mideu  28716  nbusgredgeu  29344  pjhtheu  31374  pjpreeq  31378  cnlnadjeui  32057  cvmliftlem14  35341  cvmlift2lem13  35359  cvmlift3  35372  r1peuqusdeg1  35687  linethrueu  36198  phpreu  37652  poimirlem18  37686  poimirlem21  37689  primrootsunit1  42138  addinvcom  42473  reutruALT  48844  lubeldm2  48995  glbeldm2  48996  upeu  49211