Theorem reu4 1924

Description: Restricted uniqueness using implicit substitution.

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

Proof of Theorem reu4

Step	Hyp	Ref	Expression
1		reu5 1919	. 2 |- (E!x e. A ph <-> (E.x e. A ph /\ E*x(x e. A /\ ph)))
2		rmo4.1	. . . 4 |- (x = y -> (ph <-> ps))
3	2	rmo4 1923	. . 3 |- (E*x(x e. A /\ ph) <-> A.x e. A A.y e. A ((ph /\ ps) -> x = y))
4	3	anbi2i 479	. 2 |- ((E.x e. A ph /\ E*x(x e. A /\ ph)) <-> (E.x e. A ph /\ A.x e. A A.y e. A ((ph /\ ps) -> x = y)))
5	1, 4	bitr 173	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 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E*wmo 1374  A.wral 1637  E.wrex 1638  E!wreu 1639

This theorem is referenced by:  wereu 2935  oawordeulem 4172  negeu 5327  receu 5670  lbreu 5992  uzwo5OLD 6159  creur 6673  creui 6674  minveceu 8514  hlimreu 9031  pjtheu 9150  adjvalvalt 9777  riesz4 9911  cdjreu 10264

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-cleq 1462  df-clel 1465  df-ral 1641  df-rex 1642  df-reu 1643

Copyright terms: Public domain