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

Theorem eubii 1909
 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 9 . . 3 (⊤ → (𝜑𝜓))
32eubidv 1908 . 2 (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
43trud 1252 1 (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98  ⊤wtru 1244  ∃!weu 1900 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-eu 1903 This theorem is referenced by:  cbveu  1924  2eu7  1994  reubiia  2494  cbvreu  2531  reuv  2573  euxfr2dc  2726  euxfrdc  2727  2reuswapdc  2743  reuun2  3220  zfnuleu  3881  copsexg  3981  funeu2  4927  funcnv3  4961  fneu2  5004  tz6.12  5201  f1ompt  5320  fsn  5335  climreu  9818
 Copyright terms: Public domain W3C validator