Theorem eubii 2012

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

Syntax hints:   ↔ wb 104  ⊤wtru 1333  ∃!weu 2003

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-eu 2006

This theorem is referenced by:  cbveu  2027  2eu7  2097  reubiia  2638  cbvreu  2675  reuv  2728  euxfr2dc  2893  euxfrdc  2894  2reuswapdc  2912  reuun2  3386  zfnuleu  4084  copsexg  4199  funeu2  5189  funcnv3  5225  fneu2  5268  tz6.12  5489  f1ompt  5611  fsn  5632  climreu  11171  divalgb  11789  txcn  12622