Theorem reu5 3298

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		eu5 2633	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3057	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3056	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3058	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 735	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 292	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1853   ∈ wcel 2139  ∃!weu 2607  ∃*wmo 2608  ∃wrex 3051  ∃!wreu 3052  ∃*wrmo 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-eu 2611  df-mo 2612  df-rex 3056  df-reu 3057  df-rmo 3058

This theorem is referenced by:  reurex  3299  reurmo  3300  reu4  3541  reueq  3545  reusv1  5015  reusv1OLD  5016  wereu  5262  wereu2  5263  fncnv  6123  moriotass  6803  supeu  8525  infeu  8567  resqreu  14192  sqrtneg  14207  sqreu  14299  catideu  16537  poslubd  17349  ismgmid  17465  mndideu  17505  evlseu  19718  frlmup4  20342  ply1divalg  24096  tglinethrueu  25733  foot  25813  mideu  25829  nbusgredgeu  26466  pjhtheu  28562  pjpreeq  28566  cnlnadjeui  29245  cvmliftlem14  31586  cvmlift2lem13  31604  cvmlift3  31617  nosupno  32155  nosupbday  32157  nosupbnd1  32166  nosupbnd2  32168  linethrueu  32569  phpreu  33706  poimirlem18  33740  poimirlem21  33743  2reu5a  41683  reuan  41686  2reurex  41687  2rexreu  41691  2reu1  41692