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

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

Proof of Theorem eu4
StepHypRef Expression
1 eu5 2294 . 2
2 eu4.1 . . . 4
32mo4 2316 . . 3
43anbi2i 698 . 2
51, 4bitri 252 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370  wal 1435  wex 1659  weu 2266  wmo 2267 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271 This theorem is referenced by:  euequ1OLD  2365  eueq  3249  euind  3264  uniintsn  4296  eusv1  4619  omeu  7294  eroveu  7466  climeu  13597  pceu  14759  initoeu2lem2  15861  psgneu  17098  gsumval3eu  17473  frgra3vlem2  25574  3vfriswmgralem  25577  frg2woteqm  25632  unirep  31746  rlimdmafv  38081
 Copyright terms: Public domain W3C validator