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

Theorem eubii 2165
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 2164 . 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 2156
This theorem is referenced by:  cbveu  2176  2eu7  2242  2eu8  2243  reubiia  2738  cbvreu  2775  reuv  2816  euxfr2  2963  euxfr  2964  2reuswap  2980  2reu5lem1  2983  reuun2  3464  zfnuleu  4162  copsexg  4268  reusv2lem4  4554  reusv6OLD  4561  reusv7OLD  4562  funeu2  5295  funcnv3  5327  fneu2  5365  tz6.12  5561  f1ompt  5698  fsn  5712  oeeu  6617  dfac5lem1  7766  dfac5lem5  7770  zmin  10328  climreu  12046  divalglem10  12617  divalgb  12619  txcn  17336  adjeu  22485  2reuswap2  23153  isconcl7a  26208  afveu  28121  tz6.12-1-afv  28142  bnj130  29222  bnj207  29229  bnj864  29270
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1532  df-nf 1535  df-eu 2160
  Copyright terms: Public domain W3C validator