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

Theorem eu4 2340
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 2305 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
2 eu4.1 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32mo4 2339 . . 3  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
43anbi2i 694 . 2  |-  ( ( E. x ph  /\  E* x ph )  <->  ( E. x ph  /\  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) ) )
51, 4bitri 249 1  |-  ( E! x ph  <->  ( E. x ph  /\  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1377   E.wex 1596   E!weu 2275   E*wmo 2276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280
This theorem is referenced by:  euequ1OLD  2397  eueq  3275  euind  3290  uniintsn  4319  eusv1  4641  omeu  7234  eroveu  7406  climeu  13341  pceu  14229  psgneu  16337  gsumval3eu  16710  frgra3vlem2  24705  3vfriswmgralem  24708  frg2woteqm  24764  unirep  29834  rlimdmafv  31757
  Copyright terms: Public domain W3C validator