Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  eubii GIF version

Theorem eubii 2012
 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 9 . . 3 (⊤ → (𝜑𝜓))
32eubidv 2011 . 2 (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
43mptru 1341 1 (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104  ⊤wtru 1333  ∃!weu 2003 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-eu 2006 This theorem is referenced by:  cbveu  2027  2eu7  2097  reubiia  2638  cbvreu  2675  reuv  2728  euxfr2dc  2893  euxfrdc  2894  2reuswapdc  2912  reuun2  3386  zfnuleu  4084  copsexg  4199  funeu2  5189  funcnv3  5225  fneu2  5268  tz6.12  5489  f1ompt  5611  fsn  5632  climreu  11171  divalgb  11789  txcn  12622
 Copyright terms: Public domain W3C validator