Theorem reu4 3699

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3044  ∃wrex 3053  ∃!wreu 3349  ∃*wrmo 3350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-eu 2562  df-clel 2803  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352

This theorem is referenced by:  reuind  3721  oawordeulem  8495  fin23lem23  10255  nqereu  10858  receu  11799  lbreu  12109  cju  12158  fprodser  15891  divalglem9  16347  ndvdssub  16355  qredeu  16604  pj1eu  19610  efgredeu  19666  lspsneu  21065  qtopeu  23636  qtophmeo  23737  minveclem7  25368  ig1peu  26113  coeeu  26163  plydivalg  26240  nocvxmin  27724  hlcgreu  28598  mirreu3  28634  trgcopyeu  28786  axcontlem2  28945  umgr2edg1  29191  umgr2edgneu  29194  usgredgreu  29198  uspgredg2vtxeu  29200  4cycl2vnunb  30269  frgr2wwlk1  30308  minvecolem7  30862  hlimreui  31218  riesz4i  32042  cdjreui  32411  xreceu  32892  cvmseu  35256  segconeu  35992  outsideofeu  36112  poimirlem4  37611  bfp  37811  exidu1  37843  rngoideu  37890  lshpsmreu  39095  cdleme  40547  lcfl7N  41488  mapdpg  41693  hdmap14lem6  41860  rediveud  42424  mpaaeu  43132  icceuelpart  47430  isuspgrim0lem  47886