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  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