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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1541  ∃!weu 2567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-mo 2539  df-eu 2568

This theorem is referenced by:  euorv  2613  euanv  2625  reubidva  3300  reueq1  3321  reueubd  3343  eueq2  3623  eueq3  3624  moeq3  3625  reusv2lem2  5292  reusv2lem5  5295  reuhypd  5312  feu  6595  dff3  6919  dff4  6920  omxpenlem  8746  dfac5lem5  9741  dfac5  9742  kmlem2  9765  kmlem12  9775  kmlem13  9776  initoval  17499  termoval  17500  isinito  17502  istermo  17503  initoid  17507  termoid  17508  initoeu1  17517  initoeu2  17522  termoeu1  17524  upxp  22520  edgnbusgreu  27455  nbusgredgeu0  27456  frgrncvvdeqlem2  28383  bnj852  32614  bnj1489  32749  funpartfv  33984  fsuppind  39989  fourierdlem36  43359  aiotaval  44259  eu2ndop1stv  44289  dfdfat2  44292  tz6.12-afv  44337  tz6.12-afv2  44404  dfatcolem  44419  prprsprreu  44644  prprreueq  44645  setrec2lem1  46070