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 1829	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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  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  3658  euxfr2w  3677  euxfrw  3678  euxfr2  3679  euxfr  3680  2reuswap  3703  2reuswap2  3704  2reu5lem1  3712  reuun2  4269  euelss  4276  reusv2lem4  5363  copsexgwOLD  5461  funeu2  6571  funcnv3  6615  fneu2  6655  tz6.12  6914  f1ompt  7116  fsn  7141  oeeu  8620  dfac5lem1  10209  dfac5lem5  10213  zmin  13078  climreu  15732  divalglem10  16581  divalgb  16583  dfinito2  18187  dftermo2  18188  txcn  23954  nbusgredgeu0  29958  adjeu  32500  reuxfrdf  33138  bnj130  35554  bnj207  35561  bnj864  35602  reueqi  37102  reueqbii  37103  bj-nuliota  38108  bj-axseprep  38126  poimirlem25  38700  poimirlem27  38702  dfsuccl4  39543  tfsconcatlem  44475  dfac5prim  46116  modelac8prim  46118  permac8prim  46140  aiotaval  48301  afveu  48359  tz6.12-1-afv  48380  tz6.12-afv2  48446  tz6.12-1-afv2  48447  pairreueq  48728  reutru  50050  alseubii  51139