Theorem eubidv 2586

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 1928	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		eubi 2584	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃!weu 2568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539  df-eu 2569

This theorem is referenced by:  euorv  2612  euanv  2624  reubidva  3364  reueubd  3367  reueq1OLD  3384  reueqbidv  3388  eueq2  3668  eueq3  3669  moeq3  3670  reusv2lem2  5344  reusv2lem5  5347  reuhypd  5364  feu  6710  dff3  7045  dff4  7046  omxpenlem  9006  dfac5lem5  10037  dfac5  10039  kmlem2  10062  kmlem12  10072  kmlem13  10073  initoval  17917  termoval  17918  isinito  17920  istermo  17921  initoid  17925  termoid  17926  initoeu1  17935  initoeu2  17940  termoeu1  17942  upxp  23567  edgnbusgreu  29440  nbusgredgeu0  29441  frgrncvvdeqlem2  30375  bnj852  35077  bnj1489  35212  funpartfv  36139  exeupre  38660  fsuppind  42829  wfac8prim  45239  permac8prim  45251  fourierdlem36  46383  aiotaval  47337  eu2ndop1stv  47367  dfdfat2  47370  tz6.12-afv  47415  tz6.12-afv2  47482  dfatcolem  47497  prprsprreu  47761  prprreueq  47762  initc  49332  initopropd  49484  termopropd  49485  termcterm  49754  termc2  49759  setrec2lem1  49934