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

Theorem eubii 2152
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 10 . . 3  |-  (  T. 
->  ( ph  <->  ps )
)
32eubidv 2151 . 2  |-  (  T. 
->  ( E! x ph  <->  E! x ps ) )
43trud 1314 1  |-  ( E! x ph  <->  E! x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    T. wtru 1307   E!weu 2143
This theorem is referenced by:  cbveu  2163  2eu7  2229  2eu8  2230  reubiia  2725  cbvreu  2762  reuv  2803  euxfr2  2950  euxfr  2951  2reuswap  2967  2reu5lem1  2970  reuun2  3451  zfnuleu  4146  copsexg  4252  reusv2lem4  4538  reusv6OLD  4545  reusv7OLD  4546  funeu2  5279  funcnv3  5311  fneu2  5349  tz6.12  5545  f1ompt  5682  fsn  5696  oeeu  6601  dfac5lem1  7750  dfac5lem5  7754  zmin  10312  climreu  12030  divalglem10  12601  divalgb  12603  txcn  17320  adjeu  22469  2reuswap2  23137  isconcl7a  26105  bnj130  28906  bnj207  28913  bnj864  28954
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1529  df-nf 1532  df-eu 2147
  Copyright terms: Public domain W3C validator