Theorem eubidv 2613

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃!weu 2595

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2566  df-eu 2596

This theorem is used by:  euorv  2639  euanv  2651  reubidva  3381  reueubd  3384  reueqbidv  3403  eueq2  3671  eueq3  3672  moeq3  3673  reusv2lem2  5368  reusv2lem5  5371  reuhypd  5388  feu  6755  dff3  7097  dff4  7098  omxpenlem  9080  dfac5lem5  10134  dfac5  10135  kmlem2  10158  kmlem12  10168  kmlem13  10169  initoval  18088  termoval  18089  isinito  18091  istermo  18092  initoid  18096  termoid  18097  initoeu1  18106  initoeu2  18111  termoeu1  18113  upxp  23855  edgnbusgreu  29835  nbusgredgeu0  29836  frgrncvvdeqlem2  30788  bnj852  35438  bnj1489  35573  funpartfv  36532  exeupre  39247  fsuppind  43444  wfac8prim  45833  permac8prim  45845  fourierdlem36  46979  aiotaval  47991  eu2ndop1stv  48021  dfdfat2  48024  tz6.12-afv  48069  tz6.12-afv2  48136  dfatcolem  48151  prprsprreu  48427  prprreueq  48428  initc  50025  initopropd  50177  termopropd  50178  termcterm  50447  termc2  50452  setrec2lem1  50627