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

Theorem eubii 2285
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 2283 . 2  |-  ( T. 
->  ( E! x ph  <->  E! x ps ) )
43trud 1379 1  |-  ( E! x ph  <->  E! x ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1371   E!weu 2260
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-tru 1373  df-ex 1588  df-nf 1591  df-eu 2264
This theorem is referenced by:  cbveu  2303  2eu7  2380  2eu8  2381  reubiia  3004  cbvreu  3043  reuv  3086  euxfr2  3243  euxfr  3244  2reuswap  3261  2reu5lem1  3264  reuun2  3733  zfnuleu  4518  reusv2lem4  4596  reusv6OLD  4603  reusv7OLD  4604  copsexg  4676  copsexgOLD  4677  funeu2  5543  funcnv3  5579  fneu2  5616  tz6.12  5808  f1ompt  5966  fsn  5982  oeeu  7144  dfac5lem1  8396  dfac5lem5  8400  zmin  11052  climreu  13138  divalglem10  13710  divalgb  13712  txcn  19317  adjeu  25430  2reuswap2  26009  afveu  30199  tz6.12-1-afv  30220  bnj130  32169  bnj207  32176  bnj864  32217  bj-nuliota  32823
  Copyright terms: Public domain W3C validator