Theorem eubidv 2575

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1532  ∃!weu 2557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-mo 2529  df-eu 2558

This theorem is referenced by:  euorv  2603  euanv  2615  reubidva  3387  reueubd  3390  reueq1OLD  3412  eueq2  3703  eueq3  3704  moeq3  3705  reusv2lem2  5393  reusv2lem5  5396  reuhypd  5413  feu  6767  dff3  7104  dff4  7105  omxpenlem  9089  dfac5lem5  10142  dfac5  10143  kmlem2  10166  kmlem12  10176  kmlem13  10177  initoval  17973  termoval  17974  isinito  17976  istermo  17977  initoid  17981  termoid  17982  initoeu1  17991  initoeu2  17996  termoeu1  17998  upxp  23514  edgnbusgreu  29167  nbusgredgeu0  29168  frgrncvvdeqlem2  30097  bnj852  34488  bnj1489  34623  funpartfv  35477  fsuppind  41745  fourierdlem36  45454  aiotaval  46398  eu2ndop1stv  46428  dfdfat2  46431  tz6.12-afv  46476  tz6.12-afv2  46543  dfatcolem  46558  prprsprreu  46782  prprreueq  46783  setrec2lem1  48047