Theorem eubii 2087

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 2086	. 2 ⊢ (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
4	3	mptru 1406	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1398  ∃!weu 2078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-eu 2081

This theorem is referenced by:  cbveu  2102  2eu7  2173  reubiia  2718  cbvreu  2764  reuv  2821  euxfr2dc  2990  euxfrdc  2991  2reuswapdc  3009  reuun2  3489  zfnuleu  4212  copsexg  4335  funeu2  5351  funcnv3  5391  fneu2  5436  tz6.12  5667  f1ompt  5798  fsn  5819  climreu  11877  divalgb  12506  gsum0g  13499  txcn  15025