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

Step	Hyp	Ref	Expression
1		eubii.1	. . . 4 ⊢ (φ ↔ ψ)
2	1	a1i 10	. . 3 ⊢ ( ⊤ → (φ ↔ ψ))
3	2	eubidv 2212	. 2 ⊢ ( ⊤ → (∃!xφ ↔ ∃!xψ))
4	3	trud 1323	1 ⊢ (∃!xφ ↔ ∃!xψ)

Syntax hints:   ↔ wb 176   ⊤ wtru 1316  ∃!weu 2204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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  2797  cbvreu  2834  reuv  2875  euxfr2  3022  euxfr  3023  2reuswap  3039  2reu5lem1  3042  reuun2  3539  copsexg  4608  funeu2  5133  funcnv3  5158  fneu2  5189  tz6.12  5346  fsn  5433