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

Theorem eubii 1906
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 (∃!xφ∃!xψ)

Proof of Theorem eubii
StepHypRef Expression
1 eubii.1 . . . 4 (φψ)
21a1i 9 . . 3 ( ⊤ → (φψ))
32eubidv 1905 . 2 ( ⊤ → (∃!xφ∃!xψ))
43trud 1251 1 (∃!xφ∃!xψ)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1243  ∃!weu 1897
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-eu 1900
This theorem is referenced by:  cbveu  1921  2eu7  1991  reubiia  2488  cbvreu  2525  reuv  2567  euxfr2dc  2720  euxfrdc  2721  2reuswapdc  2737  reuun2  3214  zfnuleu  3872  copsexg  3972  funeu2  4870  funcnv3  4904  fneu2  4947  tz6.12  5144  f1ompt  5263  fsn  5278
  Copyright terms: Public domain W3C validator