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

Step	Hyp	Ref	Expression
1		eu5 2310	. 2
2		eu4.1	. . . 4
3	2	mo4 2337	. . 3
4	3	anbi2i 694	. 2
5	1, 4	bitri 249	1

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