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 1830	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

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

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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  cbveu  2635  2eu7  2685  2eu8  2686  exists1  2688  reubiia  3376  cbvreu  3408  reuv  3482  reurab  3662  euxfr2w  3681  euxfrw  3682  euxfr2  3683  euxfr  3684  2reuswap  3707  2reuswap2  3708  2reu5lem1  3716  reuun2  4273  euelss  4280  reusv2lem4  5370  copsexgwOLD  5468  funeu2  6594  funcnv3  6640  fneu2  6680  tz6.12  6940  f1ompt  7143  fsn  7168  oeeu  8650  dfac5lem1  10241  dfac5lem5  10245  zmin  13111  climreu  15767  divalglem10  16616  divalgb  16618  dfinito2  18228  dftermo2  18229  txcn  24000  nbusgredgeu0  30006  adjeu  32548  reuxfrdf  33186  bnj130  35615  bnj207  35622  bnj864  35663  reueqi  37193  reueqbii  37194  bj-nuliota  38242  bj-axseprep  38260  poimirlem25  38831  poimirlem27  38833  dfsuccl4  39672  tfsconcatlem  44599  dfac5prim  46244  modelac8prim  46246  permac8prim  46268  aiotaval  48438  afveu  48496  tz6.12-1-afv  48517  tz6.12-afv2  48583  tz6.12-1-afv2  48584  pairreueq  48865  reutru  50245  alseubii  51356