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

Theorem eubii 2290
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  |-  ( ph  <->  ps )
Assertion
Ref Expression
eubii  |-  ( E! x ph  <->  E! x ps )

Proof of Theorem eubii
StepHypRef Expression
1 eubii.1 . . . 4  |-  ( ph  <->  ps )
21a1i 11 . . 3  |-  ( T. 
->  ( ph  <->  ps )
)
32eubidv 2288 . 2  |-  ( T. 
->  ( E! x ph  <->  E! x ps ) )
43trud 1390 1  |-  ( E! x ph  <->  E! x ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1382   E!weu 2266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838
This theorem depends on definitions:  df-bi 185  df-tru 1384  df-ex 1598  df-nf 1602  df-eu 2270
This theorem is referenced by:  cbveu  2305  2eu7  2369  2eu8  2370  reubiia  3027  cbvreu  3066  reuv  3109  euxfr2  3268  euxfr  3269  2reuswap  3286  2reu5lem1  3289  reuun2  3763  zfnuleu  4559  reusv2lem4  4637  reusv6OLD  4644  reusv7OLD  4645  copsexg  4718  copsexgOLD  4719  funeu2  5599  funcnv3  5635  fneu2  5672  tz6.12  5869  f1ompt  6034  fsn  6050  oeeu  7250  dfac5lem1  8502  dfac5lem5  8506  zmin  11182  climreu  13353  divalglem10  13932  divalgb  13934  txcn  19993  adjeu  26673  2reuswap2  27252  afveu  32072  tz6.12-1-afv  32093  bnj130  33639  bnj207  33646  bnj864  33687  bj-nuliota  34298
  Copyright terms: Public domain W3C validator