Theorem reu5 2752

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 2127	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 2518	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 2517	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 2519	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 460	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 212	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ∧ wa 104   ↔ wb 105  ∃wex 1541  ∃!weu 2079  ∃*wmo 2080   ∈ wcel 2202  ∃wrex 2512  ∃!wreu 2513  ∃*wrmo 2514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-rex 2517  df-reu 2518  df-rmo 2519

This theorem is referenced by:  reurex  2753  reurmo  2754  cbvreuw  2763  reu4  3001  reueq  3006  reusv1  4561  fncnv  5403  moriotass  6012  supeuti  7236  infeuti  7271  lteupri  7880  elrealeu  8092  rereceu  8152  exbtwnz  10556  rersqreu  11651  divalglemeunn  12545  divalglemeuneg  12547  bezoutlemeu  12641  pw2dvdseu  12803  ismgmid  13523  mndideu  13572  dedekindeu  15417  dedekindicclemicc  15426