Theorem eubidv 2578

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

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

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 395  df-ex 1775  df-mo 2532  df-eu 2561

This theorem is referenced by:  euorv  2604  euanv  2616  reubidva  3389  reueubd  3392  reueq1OLD  3413  eueq2  3716  eueq3  3717  moeq3  3718  reusv2lem2  5407  reusv2lem5  5410  reuhypd  5427  feu  6782  dff3  7119  dff4  7120  omxpenlem  9118  dfac5lem5  10177  dfac5  10179  kmlem2  10202  kmlem12  10212  kmlem13  10213  initoval  18036  termoval  18037  isinito  18039  istermo  18040  initoid  18044  termoid  18045  initoeu1  18054  initoeu2  18059  termoeu1  18061  upxp  23641  edgnbusgreu  29326  nbusgredgeu0  29327  frgrncvvdeqlem2  30256  bnj852  34804  bnj1489  34939  funpartfv  35816  fsuppind  42314  fourierdlem36  45834  aiotaval  46778  eu2ndop1stv  46808  dfdfat2  46811  tz6.12-afv  46856  tz6.12-afv2  46923  dfatcolem  46938  prprsprreu  47161  prprreueq  47162  setrec2lem1  48520