Theorem reu4 3400

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.)

Hypothesis

Ref	Expression
rmo4.1	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
reu4	|- ( E! x e. A ph <-> ( E. x e. A ph /\ A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) ) )

Distinct variable groups:   x, y, A   ph, y   ps, x

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem reu4

Step	Hyp	Ref	Expression
1		reu5 3159	. 2 |- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )
2		rmo4.1	. . . 4 |- ( x = y -> ( ph <-> ps ) )
3	2	rmo4 3399	. . 3 |- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )
4	3	anbi2i 730	. 2 |- ( ( E. x e. A ph /\ E* x e. A ph ) <-> ( E. x e. A ph /\ A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
5	1, 4	bitri 264	1 |- ( E! x e. A ph <-> ( E. x e. A ph /\ A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wral 2912   E.wrex 2913   E!wreu 2914   E*wrmo 2915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-cleq 2615  df-clel 2618  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920

This theorem is referenced by:  reuind  3411  oawordeulem  7634  fin23lem23  9148  nqereu  9751  receu  10672  lbreu  10973  cju  11016  fprodser  14679  divalglem9  15124  ndvdssub  15133  qredeu  15372  pj1eu  18109  efgredeu  18165  lspsneu  19123  qtopeu  21519  qtophmeo  21620  minveclem7  23206  ig1peu  23931  coeeu  23981  plydivalg  24054  hlcgreu  25513  mirreu3  25549  trgcopyeu  25698  axcontlem2  25845  umgr2edg1  26103  umgr2edgneu  26106  usgredgreu  26110  uspgredg2vtxeu  26112  4cycl2vnunb  27154  frgr2wwlk1  27193  minvecolem7  27739  hlimreui  28096  riesz4i  28922  cdjreui  29291  xreceu  29630  cvmseu  31258  nocvxmin  31894  segconeu  32118  outsideofeu  32238  poimirlem4  33413  bfp  33623  exidu1  33655  rngoideu  33702  lshpsmreu  34396  cdleme  35848  lcfl7N  36790  mapdpg  36995  hdmap14lem6  37165  mpaaeu  37720  icceuelpart  41372