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

Theorem eubii 2293
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 2291 . 2  |-  ( T. 
->  ( E! x ph  <->  E! x ps ) )
43trud 1383 1  |-  ( E! x ph  <->  E! x ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1375   E!weu 2268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-tru 1377  df-ex 1592  df-nf 1595  df-eu 2272
This theorem is referenced by:  cbveu  2311  2eu7  2388  2eu8  2389  reubiia  3040  cbvreu  3079  reuv  3122  euxfr2  3281  euxfr  3282  2reuswap  3299  2reu5lem1  3302  reuun2  3774  zfnuleu  4566  reusv2lem4  4644  reusv6OLD  4651  reusv7OLD  4652  copsexg  4725  copsexgOLD  4726  funeu2  5604  funcnv3  5640  fneu2  5677  tz6.12  5874  f1ompt  6034  fsn  6050  oeeu  7242  dfac5lem1  8493  dfac5lem5  8497  zmin  11167  climreu  13328  divalglem10  13908  divalgb  13910  txcn  19855  adjeu  26334  2reuswap2  26913  afveu  31524  tz6.12-1-afv  31545  bnj130  32886  bnj207  32893  bnj864  32934  bj-nuliota  33542
  Copyright terms: Public domain W3C validator