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

Theorem eubii 2520
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 2518 . 2 (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
43trud 1533 1 (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wtru 1524  ∃!weu 2498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-tru 1526  df-ex 1745  df-nf 1750  df-eu 2502
This theorem is referenced by:  cbveu  2534  2eu7  2588  2eu8  2589  reubiia  3157  cbvreu  3199  reuv  3252  euxfr2  3424  euxfr  3425  2reuswap  3443  2reu5lem1  3446  reuun2  3943  euelss  3947  zfnuleu  4819  reusv2lem4  4902  copsexg  4985  funeu2  5952  funcnv3  5997  fneu2  6034  tz6.12  6249  f1ompt  6422  fsn  6442  oeeu  7728  dfac5lem1  8984  dfac5lem5  8988  zmin  11822  climreu  14331  divalglem10  15172  divalgb  15174  txcn  21477  nbusgredgeu0  26314  adjeu  28876  2reuswap2  29455  bnj130  31070  bnj207  31077  bnj864  31118  bj-nuliota  33144  poimirlem25  33564  poimirlem27  33566  afveu  41554  tz6.12-1-afv  41575
  Copyright terms: Public domain W3C validator