Theorem eubidv 2587

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃!weu 2569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570

This theorem is referenced by:  euorv  2613  euanv  2625  reubidva  3357  reueubd  3360  reueqbidv  3379  eueq2  3657  eueq3  3658  moeq3  3659  reusv2lem2  5334  reusv2lem5  5337  reuhypd  5354  feu  6708  dff3  7044  dff4  7045  omxpenlem  9007  dfac5lem5  10038  dfac5  10040  kmlem2  10063  kmlem12  10073  kmlem13  10074  initoval  17949  termoval  17950  isinito  17952  istermo  17953  initoid  17957  termoid  17958  initoeu1  17967  initoeu2  17972  termoeu1  17974  upxp  23597  edgnbusgreu  29455  nbusgredgeu0  29456  frgrncvvdeqlem2  30390  bnj852  35084  bnj1489  35219  funpartfv  36148  exeupre  38823  fsuppind  43034  wfac8prim  45444  permac8prim  45456  fourierdlem36  46586  aiotaval  47540  eu2ndop1stv  47570  dfdfat2  47573  tz6.12-afv  47618  tz6.12-afv2  47685  dfatcolem  47700  prprsprreu  47976  prprreueq  47977  initc  49563  initopropd  49715  termopropd  49716  termcterm  49985  termc2  49990  setrec2lem1  50165