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

Theorem eubii 2666
Description: Introduce unique existential 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 2647 . 2 (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
43mptru 1645 1 (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wtru 1638  ∃!weu 2641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-tru 1641  df-ex 1860  df-mo 2635  df-eu 2642
This theorem is referenced by:  cbveu  2679  2eu7  2734  2eu8  2735  reuanid  3119  reubiia  3327  cbvreu  3369  reuv  3426  euxfr2  3600  euxfr  3601  2reuswap  3619  2reu5lem1  3622  reuun2  4122  euelss  4126  zfnuleuOLD  4993  reusv2lem4  5083  copsexg  5158  funeu2  6137  funcnv3  6180  fneu2  6217  tz6.12  6441  f1ompt  6613  fsn  6635  oeeu  7930  dfac5lem1  9239  dfac5lem5  9243  zmin  12023  climreu  14530  divalglem10  15365  divalgb  15367  txcn  21664  nbusgredgeu0  26509  adjeu  29099  2reuswap2  29677  bnj130  31289  bnj207  31296  bnj864  31337  bj-nuliota  33348  poimirlem25  33766  poimirlem27  33768  aiotaval  41695  afveu  41760  tz6.12-1-afv  41781  tz6.12-afv2  41847  tz6.12-1-afv2  41848
  Copyright terms: Public domain W3C validator