MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eu4 Structured version   Unicode version

Theorem eu4 2322
Description: Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)
Hypothesis
Ref Expression
eu4.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
eu4  |-  ( E! x ph  <->  ( E. x ph  /\  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) ) )
Distinct variable groups:    x, y    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem eu4
StepHypRef Expression
1 eu5 2321 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
2 eu4.1 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32mo4 2316 . . 3  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
43anbi2i 677 . 2  |-  ( ( E. x ph  /\  E* x ph )  <->  ( E. x ph  /\  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) ) )
51, 4bitri 242 1  |-  ( E! x ph  <->  ( E. x ph  /\  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360   A.wal 1550   E.wex 1551   E!weu 2283   E*wmo 2284
This theorem is referenced by:  euequ1  2371  eueq  3108  euind  3123  uniintsn  4089  eusv1  4719  omeu  6830  eroveu  7001  climeu  12351  pceu  13222  gsumval3eu  15515  unirep  26416  psgneu  27408  rlimdmafv  28019  frgra3vlem2  28393  3vfriswmgralem  28396  frg2woteqm  28450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288
  Copyright terms: Public domain W3C validator