Theorem eubidv 2585

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

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

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 2539  df-eu 2568

This theorem is referenced by:  euorv  2611  euanv  2623  reubidva  3375  reueubd  3378  reueq1OLD  3398  reueqbidv  3402  eueq2  3693  eueq3  3694  moeq3  3695  reusv2lem2  5369  reusv2lem5  5372  reuhypd  5389  feu  6754  dff3  7090  dff4  7091  omxpenlem  9087  dfac5lem5  10141  dfac5  10143  kmlem2  10166  kmlem12  10176  kmlem13  10177  initoval  18006  termoval  18007  isinito  18009  istermo  18010  initoid  18014  termoid  18015  initoeu1  18024  initoeu2  18029  termoeu1  18031  upxp  23561  edgnbusgreu  29346  nbusgredgeu0  29347  frgrncvvdeqlem2  30281  bnj852  34952  bnj1489  35087  funpartfv  35963  fsuppind  42613  wfac8prim  45027  fourierdlem36  46172  aiotaval  47124  eu2ndop1stv  47154  dfdfat2  47157  tz6.12-afv  47202  tz6.12-afv2  47269  dfatcolem  47284  prprsprreu  47533  prprreueq  47534  initopropd  49160  termopropd  49161  termcterm  49398  termc2  49403  setrec2lem1  49557