New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  eubii GIF version

Theorem eubii 2213
 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 10 . . 3 ( ⊤ → (φψ))
32eubidv 2212 . 2 ( ⊤ → (∃!xφ∃!xψ))
43trud 1323 1 (∃!xφ∃!xψ)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ⊤ wtru 1316  ∃!weu 2204 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-tru 1319  df-ex 1542  df-nf 1545  df-eu 2208 This theorem is referenced by:  cbveu  2224  2eu7  2290  2eu8  2291  reubiia  2796  cbvreu  2833  reuv  2874  euxfr2  3021  euxfr  3022  2reuswap  3038  2reu5lem1  3041  reuun2  3538  copsexg  4607  funeu2  5132  funcnv3  5157  fneu2  5188  tz6.12  5345  fsn  5432
 Copyright terms: Public domain W3C validator