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  5342  reusv2lem5  5345  reuhypd  5362  feu  6717  dff3  7053  dff4  7054  omxpenlem  9016  dfac5lem5  10049  dfac5  10051  kmlem2  10074  kmlem12  10084  kmlem13  10085  initoval  17960  termoval  17961  isinito  17963  istermo  17964  initoid  17968  termoid  17969  initoeu1  17978  initoeu2  17983  termoeu1  17985  upxp  23588  edgnbusgreu  29436  nbusgredgeu0  29437  frgrncvvdeqlem2  30370  bnj852  35063  bnj1489  35198  funpartfv  36127  exeupre  38812  fsuppind  43023  wfac8prim  45429  permac8prim  45441  fourierdlem36  46571  aiotaval  47537  eu2ndop1stv  47567  dfdfat2  47570  tz6.12-afv  47615  tz6.12-afv2  47682  dfatcolem  47697  prprsprreu  47973  prprreueq  47974  initc  49560  initopropd  49712  termopropd  49713  termcterm  49982  termc2  49987  setrec2lem1  50162