Theorem reu4 3677

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wral 3061  ∃wrex 3070  ∃!wreu 3347  ∃*wrmo 3348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-mo 2538  df-eu 2567  df-clel 2814  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350

This theorem is referenced by:  reuind  3699  oawordeulem  8457  fin23lem23  10184  nqereu  10787  receu  11722  lbreu  12027  cju  12071  fprodser  15759  divalglem9  16210  ndvdssub  16218  qredeu  16461  pj1eu  19398  efgredeu  19454  lspsneu  20492  qtopeu  22974  qtophmeo  23075  minveclem7  24706  ig1peu  25443  coeeu  25493  plydivalg  25566  nocvxmin  27025  hlcgreu  27269  mirreu3  27305  trgcopyeu  27457  axcontlem2  27623  umgr2edg1  27868  umgr2edgneu  27871  usgredgreu  27875  uspgredg2vtxeu  27877  4cycl2vnunb  28943  frgr2wwlk1  28982  minvecolem7  29534  hlimreui  29890  riesz4i  30714  cdjreui  31083  xreceu  31483  cvmseu  33537  segconeu  34452  outsideofeu  34572  poimirlem4  35937  bfp  36138  exidu1  36170  rngoideu  36217  lshpsmreu  37427  cdleme  38879  lcfl7N  39820  mapdpg  40025  hdmap14lem6  40192  mpaaeu  41289  icceuelpart  45306