Theorem reu4 3725

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.)

Hypothesis

Ref	Expression
rmo4.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
reu4	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem reu4

Step	Hyp	Ref	Expression
1		reu5 3367	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3724	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
4	3	anbi2i 621	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
5	1, 4	bitri 274	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394  ∀wral 3051  ∃wrex 3060  ∃!wreu 3363  ∃*wrmo 3364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-mo 2529  df-eu 2558  df-clel 2803  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366

This theorem is referenced by:  reuind  3747  oawordeulem  8574  fin23lem23  10358  nqereu  10961  receu  11898  lbreu  12208  cju  12252  fprodser  15944  divalglem9  16396  ndvdssub  16404  qredeu  16652  pj1eu  19688  efgredeu  19744  lspsneu  21098  qtopeu  23706  qtophmeo  23807  minveclem7  25449  ig1peu  26197  coeeu  26247  plydivalg  26322  nocvxmin  27803  hlcgreu  28540  mirreu3  28576  trgcopyeu  28728  axcontlem2  28894  umgr2edg1  29142  umgr2edgneu  29145  usgredgreu  29149  uspgredg2vtxeu  29151  4cycl2vnunb  30218  frgr2wwlk1  30257  minvecolem7  30811  hlimreui  31167  riesz4i  31991  cdjreui  32360  xreceu  32784  cvmseu  35115  segconeu  35846  outsideofeu  35966  poimirlem4  37336  bfp  37536  exidu1  37568  rngoideu  37615  lshpsmreu  38818  cdleme  40270  lcfl7N  41211  mapdpg  41416  hdmap14lem6  41583  mpaaeu  42846  icceuelpart  47042  isuspgrim0lem  47484