Theorem eubii 2610

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

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

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 2564  df-eu 2594

This theorem is used by:  cbveu  2632  2eu7  2682  2eu8  2683  exists1  2685  reubiia  3372  cbvreu  3404  reuv  3478  reurab  3659  euxfr2w  3678  euxfrw  3679  euxfr2  3680  euxfr  3681  2reuswap  3704  2reuswap2  3705  2reu5lem1  3713  reuun2  4271  euelss  4278  reusv2lem4  5366  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  funeu2  6560  funcnv3  6604  fneu2  6644  tz6.12  6903  f1ompt  7105  fsn  7130  oeeu  8592  dfac5lem1  10127  dfac5lem5  10131  zmin  12994  climreu  15644  divalglem10  16493  divalgb  16495  dfinito2  18093  dftermo2  18094  txcn  23853  nbusgredgeu0  29829  adjeu  32371  reuxfrdf  32967  bnj130  35384  bnj207  35391  bnj864  35432  reueqi  36810  reueqbii  36811  bj-nuliota  37802  bj-axseprep  37820  poimirlem25  38395  poimirlem27  38397  dfsuccl4  39223  tfsconcatlem  44178  dfac5prim  45814  modelac8prim  45816  permac8prim  45838  aiotaval  47984  afveu  48042  tz6.12-1-afv  48063  tz6.12-afv2  48129  tz6.12-1-afv2  48130  pairreueq  48411  reutru  49733  alseubii  50762