Theorem eubidv 2580

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  ∃!weu 2562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2534  df-eu 2563

This theorem is referenced by:  euorv  2606  euanv  2618  reubidva  3372  reueubd  3375  reueq1OLD  3393  reueqbidv  3397  eueq2  3684  eueq3  3685  moeq3  3686  reusv2lem2  5357  reusv2lem5  5360  reuhypd  5377  feu  6739  dff3  7075  dff4  7076  omxpenlem  9047  dfac5lem5  10087  dfac5  10089  kmlem2  10112  kmlem12  10122  kmlem13  10123  initoval  17962  termoval  17963  isinito  17965  istermo  17966  initoid  17970  termoid  17971  initoeu1  17980  initoeu2  17985  termoeu1  17987  upxp  23517  edgnbusgreu  29301  nbusgredgeu0  29302  frgrncvvdeqlem2  30236  bnj852  34918  bnj1489  35053  funpartfv  35940  fsuppind  42585  wfac8prim  44999  permac8prim  45011  fourierdlem36  46148  aiotaval  47100  eu2ndop1stv  47130  dfdfat2  47133  tz6.12-afv  47178  tz6.12-afv2  47245  dfatcolem  47260  prprsprreu  47524  prprreueq  47525  initc  49084  initopropd  49236  termopropd  49237  termcterm  49506  termc2  49511  setrec2lem1  49686