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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3051  ∃wrex 3061  ∃!wreu 3340  ∃*wrmo 3341

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 2539  df-eu 2569  df-clel 2811  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343

This theorem is referenced by:  reuind  3699  oawordeulem  8489  fin23lem23  10248  nqereu  10852  receu  11795  lbreu  12106  cju  12155  fprodser  15914  divalglem9  16370  ndvdssub  16378  qredeu  16627  pj1eu  19671  efgredeu  19727  lspsneu  21121  qtopeu  23681  qtophmeo  23782  minveclem7  25402  ig1peu  26140  coeeu  26190  plydivalg  26265  nocvxmin  27747  hlcgreu  28686  mirreu3  28722  trgcopyeu  28874  axcontlem2  29034  umgr2edg1  29280  umgr2edgneu  29283  usgredgreu  29287  uspgredg2vtxeu  29289  4cycl2vnunb  30360  frgr2wwlk1  30399  minvecolem7  30954  hlimreui  31310  riesz4i  32134  cdjreui  32503  xreceu  32981  cvmseu  35458  segconeu  36193  outsideofeu  36313  poimirlem4  37945  bfp  38145  exidu1  38177  rngoideu  38224  lshpsmreu  39555  cdleme  41006  lcfl7N  41947  mapdpg  42152  hdmap14lem6  42319  rediveud  42875  mpaaeu  43578  icceuelpart  47896  isuspgrim0lem  48369