Theorem eubii 2028

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

Step	Hyp	Ref	Expression
1		eubii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	eubidv 2027	. 2 ⊢ (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
4	3	mptru 1357	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 104  ⊤wtru 1349  ∃!weu 2019

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-eu 2022

This theorem is referenced by:  cbveu  2043  2eu7  2113  reubiia  2654  cbvreu  2694  reuv  2749  euxfr2dc  2915  euxfrdc  2916  2reuswapdc  2934  reuun2  3410  zfnuleu  4113  copsexg  4229  funeu2  5224  funcnv3  5260  fneu2  5303  tz6.12  5524  f1ompt  5647  fsn  5668  climreu  11260  divalgb  11884  txcn  13069