Theorem eubii 2086

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

Syntax hints:   ↔ wb 105  ⊤wtru 1396  ∃!weu 2077

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-eu 2080

This theorem is referenced by:  cbveu  2101  2eu7  2172  reubiia  2717  cbvreu  2763  reuv  2819  euxfr2dc  2988  euxfrdc  2989  2reuswapdc  3007  reuun2  3487  zfnuleu  4208  copsexg  4330  funeu2  5344  funcnv3  5383  fneu2  5428  tz6.12  5657  f1ompt  5788  fsn  5809  climreu  11823  divalgb  12451  gsum0g  13444  txcn  14964