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 3345	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3690	. . 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 3341  ∃*wrmo 3342

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 3343  df-reu 3344

This theorem is referenced by:  reuind  3713  oawordeulem  8472  fin23lem23  10220  nqereu  10823  receu  11765  lbreu  12075  cju  12124  fprodser  15856  divalglem9  16312  ndvdssub  16320  qredeu  16569  pj1eu  19575  efgredeu  19631  lspsneu  21030  qtopeu  23601  qtophmeo  23702  minveclem7  25333  ig1peu  26078  coeeu  26128  plydivalg  26205  nocvxmin  27689  hlcgreu  28563  mirreu3  28599  trgcopyeu  28751  axcontlem2  28910  umgr2edg1  29156  umgr2edgneu  29159  usgredgreu  29163  uspgredg2vtxeu  29165  4cycl2vnunb  30234  frgr2wwlk1  30273  minvecolem7  30827  hlimreui  31183  riesz4i  32007  cdjreui  32376  xreceu  32862  cvmseu  35253  segconeu  35989  outsideofeu  36109  poimirlem4  37608  bfp  37808  exidu1  37840  rngoideu  37887  lshpsmreu  39092  cdleme  40543  lcfl7N  41484  mapdpg  41689  hdmap14lem6  41856  rediveud  42420  mpaaeu  43127  icceuelpart  47424  isuspgrim0lem  47881