Theorem eubidv 2579

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  ∃!weu 2561

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2533  df-eu 2562

This theorem is referenced by:  euorv  2607  euanv  2619  reubidva  3391  reueubd  3394  reueq1OLD  3416  eueq2  3702  eueq3  3703  moeq3  3704  reusv2lem2  5390  reusv2lem5  5393  reuhypd  5410  feu  6754  dff3  7086  dff4  7087  omxpenlem  9056  dfac5lem5  10104  dfac5  10105  kmlem2  10128  kmlem12  10138  kmlem13  10139  initoval  17925  termoval  17926  isinito  17928  istermo  17929  initoid  17933  termoid  17934  initoeu1  17943  initoeu2  17948  termoeu1  17950  upxp  23056  edgnbusgreu  28489  nbusgredgeu0  28490  frgrncvvdeqlem2  29418  bnj852  33763  bnj1489  33898  funpartfv  34747  fsuppind  40951  fourierdlem36  44632  aiotaval  45575  eu2ndop1stv  45605  dfdfat2  45608  tz6.12-afv  45653  tz6.12-afv2  45720  dfatcolem  45735  prprsprreu  45959  prprreueq  45960  setrec2lem1  47386