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

Theorem eubii 1984
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 1983 . 2 (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
43mptru 1323 1 (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wtru 1315  ∃!weu 1975
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-eu 1978
This theorem is referenced by:  cbveu  1999  2eu7  2069  reubiia  2590  cbvreu  2627  reuv  2677  euxfr2dc  2840  euxfrdc  2841  2reuswapdc  2859  reuun2  3327  zfnuleu  4020  copsexg  4134  funeu2  5117  funcnv3  5153  fneu2  5196  tz6.12  5415  f1ompt  5537  fsn  5558  climreu  11006  divalgb  11518  txcn  12339
  Copyright terms: Public domain W3C validator