Theorem reu4 3666

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-mo 2540  df-eu 2569  df-clel 2816  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072

This theorem is referenced by:  reuind  3688  oawordeulem  8385  fin23lem23  10082  nqereu  10685  receu  11620  lbreu  11925  cju  11969  fprodser  15659  divalglem9  16110  ndvdssub  16118  qredeu  16363  pj1eu  19302  efgredeu  19358  lspsneu  20385  qtopeu  22867  qtophmeo  22968  minveclem7  24599  ig1peu  25336  coeeu  25386  plydivalg  25459  hlcgreu  26979  mirreu3  27015  trgcopyeu  27167  axcontlem2  27333  umgr2edg1  27578  umgr2edgneu  27581  usgredgreu  27585  uspgredg2vtxeu  27587  4cycl2vnunb  28654  frgr2wwlk1  28693  minvecolem7  29245  hlimreui  29601  riesz4i  30425  cdjreui  30794  xreceu  31196  cvmseu  33238  nocvxmin  33973  segconeu  34313  outsideofeu  34433  poimirlem4  35781  bfp  35982  exidu1  36014  rngoideu  36061  lshpsmreu  37123  cdleme  38574  lcfl7N  39515  mapdpg  39720  hdmap14lem6  39887  mpaaeu  40975  icceuelpart  44888