Theorem eubidv 2580

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃!weu 2562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2534  df-eu 2563

This theorem is referenced by:  euorv  2606  euanv  2618  reubidva  3358  reueubd  3361  reueq1OLD  3378  reueqbidv  3382  eueq2  3667  eueq3  3668  moeq3  3669  reusv2lem2  5335  reusv2lem5  5338  reuhypd  5355  feu  6695  dff3  7028  dff4  7029  omxpenlem  8986  dfac5lem5  10010  dfac5  10012  kmlem2  10035  kmlem12  10045  kmlem13  10046  initoval  17892  termoval  17893  isinito  17895  istermo  17896  initoid  17900  termoid  17901  initoeu1  17910  initoeu2  17915  termoeu1  17917  upxp  23531  edgnbusgreu  29338  nbusgredgeu0  29339  frgrncvvdeqlem2  30270  bnj852  34923  bnj1489  35058  funpartfv  35958  fsuppind  42602  wfac8prim  45014  permac8prim  45026  fourierdlem36  46160  aiotaval  47105  eu2ndop1stv  47135  dfdfat2  47138  tz6.12-afv  47183  tz6.12-afv2  47250  dfatcolem  47265  prprsprreu  47529  prprreueq  47530  initc  49102  initopropd  49254  termopropd  49255  termcterm  49524  termc2  49529  setrec2lem1  49704