Theorem eubii 2613

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		eubi 2612	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
2		eubii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1827	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 209  ∃!weu 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-eu 2597

This theorem is referenced by:  cbveu  2635  2eu7  2685  2eu8  2686  exists1  2688  reubiia  3376  cbvreu  3408  reuv  3483  reurab  3664  euxfr2w  3683  euxfrw  3684  euxfr2  3685  euxfr  3686  2reuswap  3709  2reuswap2  3710  2reu5lem1  3718  reuun2  4278  euelss  4285  reusv2lem4  5372  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  funeu2  6562  funcnv3  6606  fneu2  6646  tz6.12  6905  f1ompt  7106  fsn  7131  oeeu  8585  dfac5lem1  10103  dfac5lem5  10107  zmin  12963  climreu  15603  divalglem10  16455  divalgb  16457  dfinito2  18055  dftermo2  18056  txcn  23783  nbusgredgeu0  29718  adjeu  32241  reuxfrdf  32837  bnj130  35262  bnj207  35269  bnj864  35310  reueqi  36701  reueqbii  36702  bj-nuliota  37693  bj-axseprep  37711  poimirlem25  38296  poimirlem27  38298  dfsuccl4  39123  tfsconcatlem  44063  dfac5prim  45699  modelac8prim  45701  permac8prim  45723  aiotaval  47832  afveu  47890  tz6.12-1-afv  47911  tz6.12-afv2  47977  tz6.12-1-afv2  47978  pairreueq  48259  reutru  49582  alseubii  50610