Theorem reu4 3691

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3052  ∃wrex 3062  ∃!wreu 3350  ∃*wrmo 3351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570  df-clel 2812  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353

This theorem is referenced by:  reuind  3713  oawordeulem  8491  fin23lem23  10248  nqereu  10852  receu  11794  lbreu  12104  cju  12153  fprodser  15884  divalglem9  16340  ndvdssub  16348  qredeu  16597  pj1eu  19637  efgredeu  19693  lspsneu  21090  qtopeu  23672  qtophmeo  23773  minveclem7  25403  ig1peu  26148  coeeu  26198  plydivalg  26275  nocvxmin  27763  hlcgreu  28702  mirreu3  28738  trgcopyeu  28890  axcontlem2  29050  umgr2edg1  29296  umgr2edgneu  29299  usgredgreu  29303  uspgredg2vtxeu  29305  4cycl2vnunb  30377  frgr2wwlk1  30416  minvecolem7  30971  hlimreui  31327  riesz4i  32151  cdjreui  32520  xreceu  33014  cvmseu  35492  segconeu  36227  outsideofeu  36347  poimirlem4  37875  bfp  38075  exidu1  38107  rngoideu  38154  lshpsmreu  39485  cdleme  40936  lcfl7N  41877  mapdpg  42082  hdmap14lem6  42249  rediveud  42813  mpaaeu  43507  icceuelpart  47796  isuspgrim0lem  48253