Theorem reu5 3353

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃*wmo 2531  ∃!weu 2561  ∃wrex 3053  ∃!wreu 3349  ∃*wrmo 3350

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 2562  df-rex 3054  df-rmo 3351  df-reu 3352

This theorem is referenced by:  reurmo  3354  reurex  3355  cbvreuw  3379  reueq1  3385  reueq1f  3393  reu4  3699  reueq  3705  2reu5a  3712  2reurex  3728  2rexreu  3730  reuan  3856  2reu1  3857  reusv1  5347  wereu  5627  wereu2  5628  fncnv  6573  moriotass  7358  supeu  9381  infeu  9425  ttrcltr  9645  resqreu  15194  sqrtneg  15209  sqreu  15303  catideu  17612  poslubd  18348  ismgmid  18568  mndideu  18648  frlmup4  21686  evlseu  21966  ply1divalg  26019  2sqreulem1  27333  2sqreunnlem1  27336  nosupno  27591  nosupbday  27593  nosupbnd1  27602  nosupbnd2  27604  noinfno  27606  noinfbday  27608  noinfbnd1  27617  noinfbnd2  27619  noreceuw  28070  tglinethrueu  28542  foot  28625  mideu  28641  nbusgredgeu  29269  pjhtheu  31296  pjpreeq  31300  cnlnadjeui  31979  cvmliftlem14  35257  cvmlift2lem13  35275  cvmlift3  35288  r1peuqusdeg1  35603  linethrueu  36117  phpreu  37571  poimirlem18  37605  poimirlem21  37608  primrootsunit1  42058  addinvcom  42393  reutruALT  48766  lubeldm2  48917  glbeldm2  48918  upeu  49133