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

Theorem eu4 2182
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 2181 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
2 eu4.1 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32mo4 2176 . . 3  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
43anbi2i 675 . 2  |-  ( ( E. x ph  /\  E* x ph )  <->  ( E. x ph  /\  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) ) )
51, 4bitri 240 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 176    /\ wa 358   A.wal 1527   E.wex 1528   E!weu 2143   E*wmo 2144
This theorem is referenced by:  euequ1  2231  eueq  2937  euind  2952  uniintsn  3899  eusv1  4528  omeu  6583  eroveu  6753  climeu  12029  pceu  12899  gsumval3eu  15190  unirep  26349  psgneu  27429  frgra3vlem2  28179  3vfriswmgralem  28182
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148
  Copyright terms: Public domain W3C validator