Theorem eubidv 2579

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  ∃!weu 2561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-eu 2562

This theorem is referenced by:  euorv  2605  euanv  2617  reubidva  3361  reueubd  3364  reueq1OLD  3381  reueqbidv  3385  eueq2  3672  eueq3  3673  moeq3  3674  reusv2lem2  5341  reusv2lem5  5344  reuhypd  5361  feu  6704  dff3  7038  dff4  7039  omxpenlem  9002  dfac5lem5  10040  dfac5  10042  kmlem2  10065  kmlem12  10075  kmlem13  10076  initoval  17918  termoval  17919  isinito  17921  istermo  17922  initoid  17926  termoid  17927  initoeu1  17936  initoeu2  17941  termoeu1  17943  upxp  23526  edgnbusgreu  29330  nbusgredgeu0  29331  frgrncvvdeqlem2  30262  bnj852  34887  bnj1489  35022  funpartfv  35918  fsuppind  42563  wfac8prim  44976  permac8prim  44988  fourierdlem36  46125  aiotaval  47080  eu2ndop1stv  47110  dfdfat2  47113  tz6.12-afv  47158  tz6.12-afv2  47225  dfatcolem  47240  prprsprreu  47504  prprreueq  47505  initc  49064  initopropd  49216  termopropd  49217  termcterm  49486  termc2  49491  setrec2lem1  49666