Theorem eubii 2615

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

This proof depends on syntax axioms:   ↔ wb 209  ∃!weu 2598

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2569  df-eu 2599

This theorem is used by:  cbveu  2637  2eu7  2687  2eu8  2688  exists1  2690  reubiia  3378  cbvreu  3410  reuv  3485  reurab  3666  euxfr2w  3685  euxfrw  3686  euxfr2  3687  euxfr  3688  2reuswap  3711  2reuswap2  3712  2reu5lem1  3720  reuun2  4278  euelss  4285  reusv2lem4  5374  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  funeu2  6566  funcnv3  6610  fneu2  6650  tz6.12  6909  f1ompt  7110  fsn  7135  oeeu  8595  dfac5lem1  10123  dfac5lem5  10127  zmin  12984  climreu  15631  divalglem10  16482  divalgb  16484  dfinito2  18082  dftermo2  18083  txcn  23834  nbusgredgeu0  29776  adjeu  32312  reuxfrdf  32908  bnj130  35327  bnj207  35334  bnj864  35375  reueqi  36758  reueqbii  36759  bj-nuliota  37750  bj-axseprep  37768  poimirlem25  38353  poimirlem27  38355  dfsuccl4  39181  tfsconcatlem  44121  dfac5prim  45757  modelac8prim  45759  permac8prim  45781  aiotaval  47890  afveu  47948  tz6.12-1-afv  47969  tz6.12-afv2  48035  tz6.12-1-afv2  48036  pairreueq  48317  reutru  49639  alseubii  50667