Theorem eubidv 2612

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557  ∃!weu 2594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-mo 2565  df-eu 2595

This theorem is referenced by:  euorv  2638  euanv  2650  reubidva  3380  reueubd  3383  reueqbidv  3402  eueq2  3672  eueq3  3673  moeq3  3674  reusv2lem2  5355  reusv2lem5  5358  reuhypd  5375  feu  6734  dff3  7075  dff4  7076  omxpenlem  9044  dfac5lem5  10078  dfac5  10080  kmlem2  10103  kmlem12  10113  kmlem13  10114  initoval  18007  termoval  18008  isinito  18010  istermo  18011  initoid  18015  termoid  18016  initoeu1  18025  initoeu2  18030  termoeu1  18032  upxp  23661  edgnbusgreu  29512  nbusgredgeu0  29513  frgrncvvdeqlem2  30446  bnj852  35178  bnj1489  35313  funpartfv  36248  exeupre  38943  fsuppind  43125  wfac8prim  45531  permac8prim  45543  fourierdlem36  46670  aiotaval  47642  eu2ndop1stv  47672  dfdfat2  47675  tz6.12-afv  47720  tz6.12-afv2  47787  dfatcolem  47802  prprsprreu  48078  prprreueq  48079  initc  49665  initopropd  49817  termopropd  49818  termcterm  50087  termc2  50092  setrec2lem1  50267