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

Theorem eu4 2338
 Description: Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)
Hypothesis
Ref Expression
eu4.1
Assertion
Ref Expression
eu4
Distinct variable groups:   ,   ,   ,

Proof of Theorem eu4
StepHypRef Expression
1 eu5 2310 . 2
2 eu4.1 . . . 4
32mo4 2337 . . 3
43anbi2i 694 . 2
51, 4bitri 249 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  E!weu 2282  E*wmo 2283 This theorem is referenced by:  euequ1OLD  2387  eueq  3271  euind  3286  uniintsn  4324  eusv1  4646  omeu  7253  eroveu  7425  climeu  13378  pceu  14370  psgneu  16531  gsumval3eu  16907  frgra3vlem2  25001  3vfriswmgralem  25004  frg2woteqm  25059  unirep  30203  rlimdmafv  32262  initoeu2lem2  32621 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287
 Copyright terms: Public domain W3C validator