Theorem eubidv 2586

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

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

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 2540  df-eu 2569

This theorem is referenced by:  euorv  2612  euanv  2624  reubidva  3396  reueubd  3399  reueq1OLD  3419  reueqbidv  3423  eueq2  3716  eueq3  3717  moeq3  3718  reusv2lem2  5399  reusv2lem5  5402  reuhypd  5419  feu  6784  dff3  7120  dff4  7121  omxpenlem  9113  dfac5lem5  10167  dfac5  10169  kmlem2  10192  kmlem12  10202  kmlem13  10203  initoval  18038  termoval  18039  isinito  18041  istermo  18042  initoid  18046  termoid  18047  initoeu1  18056  initoeu2  18061  termoeu1  18063  upxp  23631  edgnbusgreu  29384  nbusgredgeu0  29385  frgrncvvdeqlem2  30319  bnj852  34935  bnj1489  35070  funpartfv  35946  fsuppind  42600  wfac8prim  45019  fourierdlem36  46158  aiotaval  47107  eu2ndop1stv  47137  dfdfat2  47140  tz6.12-afv  47185  tz6.12-afv2  47252  dfatcolem  47267  prprsprreu  47506  prprreueq  47507  termcterm  49145  termc2  49148  setrec2lem1  49212