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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  ∃!weu 2568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-mo 2540  df-eu 2569

This theorem is referenced by:  euorv  2614  euanv  2626  reubidva  3322  reueq1  3344  reueubd  3367  eueq2  3645  eueq3  3646  moeq3  3647  reusv2lem2  5322  reusv2lem5  5325  reuhypd  5342  feu  6650  dff3  6976  dff4  6977  omxpenlem  8860  dfac5lem5  9883  dfac5  9884  kmlem2  9907  kmlem12  9917  kmlem13  9918  initoval  17708  termoval  17709  isinito  17711  istermo  17712  initoid  17716  termoid  17717  initoeu1  17726  initoeu2  17731  termoeu1  17733  upxp  22774  edgnbusgreu  27734  nbusgredgeu0  27735  frgrncvvdeqlem2  28664  bnj852  32901  bnj1489  33036  funpartfv  34247  fsuppind  40279  fourierdlem36  43684  aiotaval  44587  eu2ndop1stv  44617  dfdfat2  44620  tz6.12-afv  44665  tz6.12-afv2  44732  dfatcolem  44747  prprsprreu  44971  prprreueq  44972  setrec2lem1  46399