Theorem reu4 3687

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3049  ∃wrex 3058  ∃!wreu 3346  ∃*wrmo 3347

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 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2537  df-eu 2566  df-clel 2808  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349

This theorem is referenced by:  reuind  3709  oawordeulem  8478  fin23lem23  10227  nqereu  10830  receu  11772  lbreu  12082  cju  12131  fprodser  15866  divalglem9  16322  ndvdssub  16330  qredeu  16579  pj1eu  19618  efgredeu  19674  lspsneu  21070  qtopeu  23641  qtophmeo  23742  minveclem7  25372  ig1peu  26117  coeeu  26167  plydivalg  26244  nocvxmin  27728  hlcgreu  28606  mirreu3  28642  trgcopyeu  28794  axcontlem2  28954  umgr2edg1  29200  umgr2edgneu  29203  usgredgreu  29207  uspgredg2vtxeu  29209  4cycl2vnunb  30281  frgr2wwlk1  30320  minvecolem7  30874  hlimreui  31230  riesz4i  32054  cdjreui  32423  xreceu  32913  cvmseu  35331  segconeu  36066  outsideofeu  36186  poimirlem4  37674  bfp  37874  exidu1  37906  rngoideu  37953  lshpsmreu  39218  cdleme  40669  lcfl7N  41610  mapdpg  41815  hdmap14lem6  41982  rediveud  42551  mpaaeu  43257  icceuelpart  47550  isuspgrim0lem  48007