Theorem reu4 3737

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3061  ∃wrex 3070  ∃!wreu 3378  ∃*wrmo 3379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-eu 2569  df-clel 2816  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381

This theorem is referenced by:  reuind  3759  oawordeulem  8592  fin23lem23  10366  nqereu  10969  receu  11908  lbreu  12218  cju  12262  fprodser  15985  divalglem9  16438  ndvdssub  16446  qredeu  16695  pj1eu  19714  efgredeu  19770  lspsneu  21125  qtopeu  23724  qtophmeo  23825  minveclem7  25469  ig1peu  26214  coeeu  26264  plydivalg  26341  nocvxmin  27823  hlcgreu  28626  mirreu3  28662  trgcopyeu  28814  axcontlem2  28980  umgr2edg1  29228  umgr2edgneu  29231  usgredgreu  29235  uspgredg2vtxeu  29237  4cycl2vnunb  30309  frgr2wwlk1  30348  minvecolem7  30902  hlimreui  31258  riesz4i  32082  cdjreui  32451  xreceu  32904  cvmseu  35281  segconeu  36012  outsideofeu  36132  poimirlem4  37631  bfp  37831  exidu1  37863  rngoideu  37910  lshpsmreu  39110  cdleme  40562  lcfl7N  41503  mapdpg  41708  hdmap14lem6  41875  mpaaeu  43162  icceuelpart  47423  isuspgrim0lem  47871