Theorem eubidv 2590

Description: Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.)

Hypothesis

Ref	Expression
eubidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
eubidv	⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem eubidv

Step	Hyp	Ref	Expression
1		eubidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	alrimiv 1934	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		eubi 2588	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545  ∃!weu 2572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543  df-eu 2573

This theorem is referenced by:  euorv  2616  euanv  2628  reubidva  3359  reueubd  3362  reueqbidv  3381  eueq2  3658  eueq3  3659  moeq3  3660  reusv2lem2  5335  reusv2lem5  5338  reuhypd  5355  feu  6710  dff3  7048  dff4  7049  omxpenlem  9013  dfac5lem5  10047  dfac5  10049  kmlem2  10072  kmlem12  10082  kmlem13  10083  initoval  17958  termoval  17959  isinito  17961  istermo  17962  initoid  17966  termoid  17967  initoeu1  17976  initoeu2  17981  termoeu1  17983  upxp  23613  edgnbusgreu  29461  nbusgredgeu0  29462  frgrncvvdeqlem2  30395  bnj852  35110  bnj1489  35245  funpartfv  36174  exeupre  38859  fsuppind  43041  wfac8prim  45447  permac8prim  45459  fourierdlem36  46587  aiotaval  47559  eu2ndop1stv  47589  dfdfat2  47592  tz6.12-afv  47637  tz6.12-afv2  47704  dfatcolem  47719  prprsprreu  47995  prprreueq  47996  initc  49582  initopropd  49734  termopropd  49735  termcterm  50004  termc2  50009  setrec2lem1  50184