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 2289 . 2  |-  (  T. 
->  ( E! x ph  <->  E! x ps ) )
43trud 1332 1  |-  ( E! x ph  <->  E! x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1325   E!weu 2281
This theorem is referenced by:  cbveu  2301  2eu7  2367  2eu8  2368  reubiia  2893  cbvreu  2930  reuv  2971  euxfr2  3119  euxfr  3120  2reuswap  3136  2reu5lem1  3139  reuun2  3624  zfnuleu  4335  copsexg  4442  reusv2lem4  4727  reusv6OLD  4734  reusv7OLD  4735  funeu2  5478  funcnv3  5512  fneu2  5550  tz6.12  5748  f1ompt  5891  fsn  5906  oeeu  6846  dfac5lem1  8004  dfac5lem5  8008  zmin  10570  climreu  12350  divalglem10  12922  divalgb  12924  txcn  17658  adjeu  23392  2reuswap2  23975  afveu  27993  tz6.12-1-afv  28014  bnj130  29245  bnj207  29252  bnj864  29293
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-tru 1328  df-ex 1551  df-nf 1554  df-eu 2285
  Copyright terms: Public domain W3C validator