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  28655  nbusgredgeu0  28656  frgrncvvdeqlem2  29584  bnj852  33963  bnj1489  34098  funpartfv  34948  fsuppind  41210  fourierdlem36  44907  aiotaval  45851  eu2ndop1stv  45881  dfdfat2  45884  tz6.12-afv  45929  tz6.12-afv2  45996  dfatcolem  46011  prprsprreu  46235  prprreueq  46236  setrec2lem1  47786