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

Theorem eubii 1891
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 1890 . 2 ( ⊤ → (∃!xφ∃!xψ))
43trud 1237 1 (∃!xφ∃!xψ)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1229  ∃!weu 1882
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-eu 1885
This theorem is referenced by:  cbveu  1906  2eu7  1976  reubiia  2472  cbvreu  2509  reuv  2550  euxfr2dc  2703  euxfrdc  2704  2reuswapdc  2720  reuun2  3197  zfnuleu  3855  copsexg  3955  funeu2  4853  funcnv3  4887  fneu2  4930  tz6.12  5126  f1ompt  5245  fsn  5260
  Copyright terms: Public domain W3C validator