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

Theorem eubii 2480
 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 (𝜑𝜓)
Assertion
Ref Expression
eubii (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Proof of Theorem eubii
StepHypRef Expression
1 eubii.1 . . . 4 (𝜑𝜓)
21a1i 11 . . 3 (⊤ → (𝜑𝜓))
32eubidv 2478 . 2 (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
43trud 1484 1 (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195  ⊤wtru 1476  ∃!weu 2458 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462 This theorem is referenced by:  cbveu  2493  2eu7  2547  2eu8  2548  reubiia  3104  cbvreu  3145  reuv  3194  euxfr2  3358  euxfr  3359  2reuswap  3377  2reu5lem1  3380  reuun2  3869  euelss  3873  zfnuleu  4714  reusv2lem4  4798  copsexg  4882  funeu2  5829  funcnv3  5873  fneu2  5910  tz6.12  6121  f1ompt  6290  fsn  6308  oeeu  7570  dfac5lem1  8829  dfac5lem5  8833  zmin  11660  climreu  14135  divalglem10  14963  divalgb  14965  txcn  21239  adjeu  28132  2reuswap2  28712  bnj130  30198  bnj207  30205  bnj864  30246  bj-nuliota  32210  poimirlem25  32604  poimirlem27  32606  afveu  39882  tz6.12-1-afv  39903  nbusgredgeu0  40596
 Copyright terms: Public domain W3C validator