Theorem eubii 2480

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

Syntax hints:   ↔ wb 195  ⊤wtru 1476  ∃!weu 2458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462

This theorem is referenced by:  cbveu  2493  2eu7  2547  2eu8  2548  reubiia  3104  cbvreu  3145  reuv  3194  euxfr2  3358  euxfr  3359  2reuswap  3377  2reu5lem1  3380  reuun2  3869  euelss  3873  zfnuleu  4714  reusv2lem4  4798  copsexg  4882  funeu2  5829  funcnv3  5873  fneu2  5910  tz6.12  6121  f1ompt  6290  fsn  6308  oeeu  7570  dfac5lem1  8829  dfac5lem5  8833  zmin  11660  climreu  14135  divalglem10  14963  divalgb  14965  txcn  21239  adjeu  28132  2reuswap2  28712  bnj130  30198  bnj207  30205  bnj864  30246  bj-nuliota  32210  poimirlem25  32604  poimirlem27  32606  afveu  39882  tz6.12-1-afv  39903  nbusgredgeu0  40596