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

Theorem eubii 2306
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 2304 . 2
43trud 1404 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184   wtru 1396  E!weu 2282
This theorem is referenced by:  cbveu  2321  2eu7  2385  2eu8  2386  reubiia  3043  cbvreu  3082  reuv  3125  euxfr2  3284  euxfr  3285  2reuswap  3302  2reu5lem1  3305  reuun2  3780  zfnuleu  4578  reusv2lem4  4656  reusv6OLD  4663  reusv7OLD  4664  copsexg  4737  copsexgOLD  4738  funeu2  5618  funcnv3  5654  fneu2  5691  tz6.12  5888  f1ompt  6053  fsn  6069  oeeu  7271  dfac5lem1  8525  dfac5lem5  8529  zmin  11207  climreu  13379  divalglem10  14060  divalgb  14062  txcn  20127  adjeu  26808  2reuswap2  27387  afveu  32238  tz6.12-1-afv  32259  euelss  32553  bnj130  33932  bnj207  33939  bnj864  33980  bj-nuliota  34586
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-tru 1398  df-ex 1613  df-nf 1617  df-eu 2286
  Copyright terms: Public domain W3C validator