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

Theorem eubii 2287
Description: Introduce uniqueness quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
Hypothesis
Ref Expression
eubii.1
Assertion
Ref Expression
eubii

Proof of Theorem eubii
StepHypRef Expression
1 eubii.1 . . . 4
21a1i 11 . . 3
32eubidv 2285 . 2
43trud 1379 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184   wtru 1371  E!weu 2262
This theorem is referenced by:  cbveu  2305  2eu7  2382  2eu8  2383  reubiia  3015  cbvreu  3054  reuv  3097  euxfr2  3254  euxfr  3255  2reuswap  3272  2reu5lem1  3275  reuun2  3747  zfnuleu  4535  reusv2lem4  4613  reusv6OLD  4620  reusv7OLD  4621  copsexg  4693  copsexgOLD  4694  funeu2  5562  funcnv3  5598  fneu2  5635  tz6.12  5830  f1ompt  5988  fsn  6004  oeeu  7176  dfac5lem1  8430  dfac5lem5  8434  zmin  11088  climreu  13192  divalglem10  13764  divalgb  13766  txcn  19598  adjeu  25762  2reuswap2  26341  afveu  30936  tz6.12-1-afv  30957  bnj130  32710  bnj207  32717  bnj864  32758  bj-nuliota  33366
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 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-tru 1373  df-ex 1588  df-nf 1591  df-eu 2266
  Copyright terms: Public domain W3C validator