Theorem reu4 3678

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3052  ∃wrex 3062  ∃!wreu 3341  ∃*wrmo 3342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570  df-clel 2812  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344

This theorem is referenced by:  reuind  3700  oawordeulem  8483  fin23lem23  10242  nqereu  10846  receu  11789  lbreu  12100  cju  12149  fprodser  15908  divalglem9  16364  ndvdssub  16372  qredeu  16621  pj1eu  19665  efgredeu  19721  lspsneu  21116  qtopeu  23694  qtophmeo  23795  minveclem7  25415  ig1peu  26153  coeeu  26203  plydivalg  26279  nocvxmin  27764  hlcgreu  28703  mirreu3  28739  trgcopyeu  28891  axcontlem2  29051  umgr2edg1  29297  umgr2edgneu  29300  usgredgreu  29304  uspgredg2vtxeu  29306  4cycl2vnunb  30378  frgr2wwlk1  30417  minvecolem7  30972  hlimreui  31328  riesz4i  32152  cdjreui  32521  xreceu  32999  cvmseu  35477  segconeu  36212  outsideofeu  36332  poimirlem4  37962  bfp  38162  exidu1  38194  rngoideu  38241  lshpsmreu  39572  cdleme  41023  lcfl7N  41964  mapdpg  42169  hdmap14lem6  42336  rediveud  42892  mpaaeu  43599  icceuelpart  47911  isuspgrim0lem  48384