Theorem eubidv 2581

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540  ∃!weu 2563

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 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535  df-eu 2564

This theorem is referenced by:  euorv  2609  euanv  2621  reubidva  3393  reueubd  3396  reueq1OLD  3418  eueq2  3707  eueq3  3708  moeq3  3709  reusv2lem2  5398  reusv2lem5  5401  reuhypd  5418  feu  6768  dff3  7102  dff4  7103  omxpenlem  9073  dfac5lem5  10122  dfac5  10123  kmlem2  10146  kmlem12  10156  kmlem13  10157  initoval  17943  termoval  17944  isinito  17946  istermo  17947  initoid  17951  termoid  17952  initoeu1  17961  initoeu2  17966  termoeu1  17968  upxp  23127  edgnbusgreu  28624  nbusgredgeu0  28625  frgrncvvdeqlem2  29553  bnj852  33932  bnj1489  34067  funpartfv  34917  fsuppind  41162  fourierdlem36  44859  aiotaval  45803  eu2ndop1stv  45833  dfdfat2  45836  tz6.12-afv  45881  tz6.12-afv2  45948  dfatcolem  45963  prprsprreu  46187  prprreueq  46188  setrec2lem1  47738