Theorem eubii 2520

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	⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Proof of Theorem eubii

Step	Hyp	Ref	Expression
1		eubii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	eubidv 2518	. 2 ⊢ (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
4	3	trud 1533	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 196  ⊤wtru 1524  ∃!weu 2498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-tru 1526  df-ex 1745  df-nf 1750  df-eu 2502

This theorem is referenced by:  cbveu  2534  2eu7  2588  2eu8  2589  reubiia  3157  cbvreu  3199  reuv  3252  euxfr2  3424  euxfr  3425  2reuswap  3443  2reu5lem1  3446  reuun2  3943  euelss  3947  zfnuleu  4819  reusv2lem4  4902  copsexg  4985  funeu2  5952  funcnv3  5997  fneu2  6034  tz6.12  6249  f1ompt  6422  fsn  6442  oeeu  7728  dfac5lem1  8984  dfac5lem5  8988  zmin  11822  climreu  14331  divalglem10  15172  divalgb  15174  txcn  21477  nbusgredgeu0  26314  adjeu  28876  2reuswap2  29455  bnj130  31070  bnj207  31077  bnj864  31118  bj-nuliota  33144  poimirlem25  33564  poimirlem27  33566  afveu  41554  tz6.12-1-afv  41575