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
Assertion
Ref Expression
eu4
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem eu4
StepHypRef Expression
1 eu5 2321 . 2
2 eu4.1 . . . 4
32mo4 2316 . . 3
43anbi2i 677 . 2
51, 4bitri 242 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360  wal 1550  wex 1551  weu 2283  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