Theorem eubidv 2611

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567  ∃!weu 2593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564  df-eu 2594

This theorem is used by:  euorv  2637  euanv  2649  reubidva  3379  reueubd  3382  reueqbidv  3401  eueq2  3667  eueq3  3668  moeq3  3669  reusv2lem2  5360  reusv2lem5  5363  reuhypd  5380  feu  6758  dff3  7100  dff4  7101  omxpenlem  9100  setrec2lem1  9977  dfac5lem5  10209  dfac5  10210  kmlem2  10233  kmlem12  10243  kmlem13  10244  initoval  18173  termoval  18174  isinito  18176  istermo  18177  initoid  18181  termoid  18182  initoeu1  18191  initoeu2  18196  termoeu1  18198  upxp  23947  edgnbusgreu  29953  nbusgredgeu0  29954  frgrncvvdeqlem2  30906  bnj852  35597  bnj1489  35732  funpartfv  36801  exeupre  39516  fsuppind  43711  wfac8prim  46085  permac8prim  46097  fourierdlem36  47246  aiotaval  48258  eu2ndop1stv  48288  dfdfat2  48291  tz6.12-afv  48336  tz6.12-afv2  48403  dfatcolem  48418  prprsprreu  48694  prprreueq  48695  initc  50299  initopropd  50458  termopropd  50459  termcterm  50741  termc2  50746