Theorem reu4 3661

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wral 3063  ∃wrex 3064  ∃!wreu 3065  ∃*wrmo 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-mo 2540  df-eu 2569  df-clel 2817  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071

This theorem is referenced by:  reuind  3683  oawordeulem  8347  fin23lem23  10013  nqereu  10616  receu  11550  lbreu  11855  cju  11899  fprodser  15587  divalglem9  16038  ndvdssub  16046  qredeu  16291  pj1eu  19217  efgredeu  19273  lspsneu  20300  qtopeu  22775  qtophmeo  22876  minveclem7  24504  ig1peu  25241  coeeu  25291  plydivalg  25364  hlcgreu  26883  mirreu3  26919  trgcopyeu  27071  axcontlem2  27236  umgr2edg1  27481  umgr2edgneu  27484  usgredgreu  27488  uspgredg2vtxeu  27490  4cycl2vnunb  28555  frgr2wwlk1  28594  minvecolem7  29146  hlimreui  29502  riesz4i  30326  cdjreui  30695  xreceu  31098  cvmseu  33138  nocvxmin  33900  segconeu  34240  outsideofeu  34360  poimirlem4  35708  bfp  35909  exidu1  35941  rngoideu  35988  lshpsmreu  37050  cdleme  38501  lcfl7N  39442  mapdpg  39647  hdmap14lem6  39814  mpaaeu  40891  icceuelpart  44776