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

Theorem eubidv 2304
Description: Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
Hypothesis
Ref Expression
eubidv.1
Assertion
Ref Expression
eubidv
Distinct variable group:   ,

Proof of Theorem eubidv
StepHypRef Expression
1 nfv 1707 . 2
2 eubidv.1 . 2
31, 2eubid 2302 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  E!weu 2282
This theorem is referenced by:  eubii  2306  eueq2  3273  eueq3  3274  moeq3  3276  reusv2lem2  4654  reusv2lem5  4657  reusv7OLD  4664  reuhypd  4679  feu  5766  dff3  6044  dff4  6045  omxpenlem  7638  dfac5lem5  8529  dfac5  8530  kmlem2  8552  kmlem12  8562  kmlem13  8563  upxp  20124  frgrancvvdeqlem3  25032  frgraeu  25054  funpartfv  29595  fourierdlem36  31925  eu2ndop1stv  32207  dfdfat2  32216  tz6.12-afv  32258  initoval  32603  termoval  32604  isinito  32606  istermo  32607  initoid  32611  termoid  32612  initoeu1  32617  initoeu2  32622  termoeu1  32624  bnj852  33979  bnj1489  34112
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-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-eu 2286
  Copyright terms: Public domain W3C validator