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

Theorem eu4 2324
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 2289 . 2
2 eu4.1 . . . 4
32mo4 2323 . . 3
43anbi2i 694 . 2
51, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1368  E.wex 1587  E!weu 2259  E*wmo 2260
This theorem is referenced by:  euequ1OLD  2381  eueq  3212  euind  3227  uniintsn  4247  eusv1  4568  omeu  7108  eroveu  7279  climeu  13119  pceu  13999  psgneu  16098  gsumval3eu  16469  unirep  28728  rlimdmafv  30205  frgra3vlem2  30715  3vfriswmgralem  30718  frg2woteqm  30774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264
  Copyright terms: Public domain W3C validator