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 2567  df-clel 2809  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349

This theorem is referenced by:  reuind  3709  oawordeulem  8479  fin23lem23  10234  nqereu  10838  receu  11780  lbreu  12090  cju  12139  fprodser  15870  divalglem9  16326  ndvdssub  16334  qredeu  16583  pj1eu  19623  efgredeu  19679  lspsneu  21076  qtopeu  23658  qtophmeo  23759  minveclem7  25389  ig1peu  26134  coeeu  26184  plydivalg  26261  nocvxmin  27745  hlcgreu  28639  mirreu3  28675  trgcopyeu  28827  axcontlem2  28987  umgr2edg1  29233  umgr2edgneu  29236  usgredgreu  29240  uspgredg2vtxeu  29242  4cycl2vnunb  30314  frgr2wwlk1  30353  minvecolem7  30907  hlimreui  31263  riesz4i  32087  cdjreui  32456  xreceu  32952  cvmseu  35419  segconeu  36154  outsideofeu  36274  poimirlem4  37764  bfp  37964  exidu1  37996  rngoideu  38043  lshpsmreu  39308  cdleme  40759  lcfl7N  41700  mapdpg  41905  hdmap14lem6  42072  rediveud  42640  mpaaeu  43334  icceuelpart  47624  isuspgrim0lem  48081