Theorem reu4 3724

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 3432	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3723	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
4	3	anbi2i 624	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
5	1, 4	bitri 277	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wral 3140  ∃wrex 3141  ∃!wreu 3142  ∃*wrmo 3143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622  df-eu 2654  df-clel 2895  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148

This theorem is referenced by:  reuind  3746  oawordeulem  8182  fin23lem23  9750  nqereu  10353  receu  11287  lbreu  11593  cju  11636  fprodser  15305  divalglem9  15754  ndvdssub  15762  qredeu  16004  pj1eu  18824  efgredeu  18880  lspsneu  19897  qtopeu  22326  qtophmeo  22427  minveclem7  24040  ig1peu  24767  coeeu  24817  plydivalg  24890  hlcgreu  26406  mirreu3  26442  trgcopyeu  26594  axcontlem2  26753  umgr2edg1  26995  umgr2edgneu  26998  usgredgreu  27002  uspgredg2vtxeu  27004  4cycl2vnunb  28071  frgr2wwlk1  28110  minvecolem7  28662  hlimreui  29018  riesz4i  29842  cdjreui  30211  xreceu  30600  cvmseu  32525  nocvxmin  33250  segconeu  33474  outsideofeu  33594  poimirlem4  34898  bfp  35104  exidu1  35136  rngoideu  35183  lshpsmreu  36247  cdleme  37698  lcfl7N  38639  mapdpg  38844  hdmap14lem6  39011  mpaaeu  39757  icceuelpart  43603