Theorem reu5 3375

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 2629	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3113	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3112	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3114	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 629	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃*wmo 2596  ∃!weu 2628  ∃wrex 3107  ∃!wreu 3108  ∃*wrmo 3109

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 210  df-an 400  df-eu 2629  df-rex 3112  df-reu 3113  df-rmo 3114

This theorem is referenced by:  reurex  3376  reurmo  3378  reu4  3670  reueq  3676  2reu5a  3683  2reurex  3698  2rexreu  3701  reuan  3825  2reu1  3826  reusv1  5263  wereu  5515  wereu2  5516  fncnv  6397  moriotass  7125  supeu  8902  infeu  8944  resqreu  14604  sqrtneg  14619  sqreu  14712  catideu  16938  poslubd  17750  ismgmid  17867  mndideu  17914  frlmup4  20490  evlseu  20755  ply1divalg  24738  2sqreulem1  26030  2sqreunnlem1  26033  tglinethrueu  26433  foot  26516  mideu  26532  nbusgredgeu  27156  pjhtheu  29177  pjpreeq  29181  cnlnadjeui  29860  cvmliftlem14  32657  cvmlift2lem13  32675  cvmlift3  32688  nosupno  33316  nosupbday  33318  nosupbnd1  33327  nosupbnd2  33329  linethrueu  33730  phpreu  35041  poimirlem18  35075  poimirlem21  35078  addinvcom  39568