Theorem reu4 3636

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387  ∀wral 3088  ∃wrex 3089  ∃!wreu 3090  ∃*wrmo 3091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-10 2079  ax-11 2093  ax-12 2106

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clel 2846  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096

This theorem is referenced by:  reuind  3655  oawordeulem  7983  fin23lem23  9548  nqereu  10151  receu  11088  lbreu  11394  cju  11437  fprodser  15166  divalglem9  15615  ndvdssub  15623  qredeu  15861  pj1eu  18583  efgredeu  18641  lspsneu  19620  qtopeu  22031  qtophmeo  22132  minveclem7  23744  ig1peu  24471  coeeu  24521  plydivalg  24594  hlcgreu  26109  mirreu3  26145  trgcopyeu  26297  axcontlem2  26457  umgr2edg1  26699  umgr2edgneu  26702  usgredgreu  26706  uspgredg2vtxeu  26708  4cycl2vnunb  27827  frgr2wwlk1  27866  minvecolem7  28441  hlimreui  28798  riesz4i  29624  cdjreui  29993  xreceu  30347  cvmseu  32108  nocvxmin  32769  segconeu  32993  outsideofeu  33113  poimirlem4  34337  bfp  34544  exidu1  34576  rngoideu  34623  lshpsmreu  35690  cdleme  37141  lcfl7N  38082  mapdpg  38287  hdmap14lem6  38454  mpaaeu  39146  icceuelpart  42969