Theorem eubidv 2583

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534  ∃!weu 2565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-mo 2537  df-eu 2566

This theorem is referenced by:  euorv  2609  euanv  2621  reubidva  3393  reueubd  3396  reueq1OLD  3416  eueq2  3718  eueq3  3719  moeq3  3720  reusv2lem2  5404  reusv2lem5  5407  reuhypd  5424  feu  6784  dff3  7119  dff4  7120  omxpenlem  9111  dfac5lem5  10164  dfac5  10166  kmlem2  10189  kmlem12  10199  kmlem13  10200  initoval  18046  termoval  18047  isinito  18049  istermo  18050  initoid  18054  termoid  18055  initoeu1  18064  initoeu2  18069  termoeu1  18071  upxp  23646  edgnbusgreu  29398  nbusgredgeu0  29399  frgrncvvdeqlem2  30328  bnj852  34913  bnj1489  35048  funpartfv  35926  reueqbidv  36195  fsuppind  42576  fourierdlem36  46098  aiotaval  47044  eu2ndop1stv  47074  dfdfat2  47077  tz6.12-afv  47122  tz6.12-afv2  47189  dfatcolem  47204  prprsprreu  47443  prprreueq  47444  setrec2lem1  48923