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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  ∃!weu 2568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-mo 2540  df-eu 2569

This theorem is referenced by:  euorv  2614  euanv  2626  reubidva  3314  reueq1  3335  reueubd  3357  eueq2  3640  eueq3  3641  moeq3  3642  reusv2lem2  5317  reusv2lem5  5320  reuhypd  5337  feu  6634  dff3  6958  dff4  6959  omxpenlem  8813  dfac5lem5  9814  dfac5  9815  kmlem2  9838  kmlem12  9848  kmlem13  9849  initoval  17624  termoval  17625  isinito  17627  istermo  17628  initoid  17632  termoid  17633  initoeu1  17642  initoeu2  17647  termoeu1  17649  upxp  22682  edgnbusgreu  27637  nbusgredgeu0  27638  frgrncvvdeqlem2  28565  bnj852  32801  bnj1489  32936  funpartfv  34174  fsuppind  40202  fourierdlem36  43574  aiotaval  44474  eu2ndop1stv  44504  dfdfat2  44507  tz6.12-afv  44552  tz6.12-afv2  44619  dfatcolem  44634  prprsprreu  44859  prprreueq  44860  setrec2lem1  46285