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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2565  df-eu 2595

This theorem is used by:  euorv  2638  euanv  2650  reubidva  3380  reueubd  3383  reueqbidv  3402  eueq2  3668  eueq3  3669  moeq3  3670  reusv2lem2  5361  reusv2lem5  5364  reuhypd  5381  feu  6750  dff3  7092  dff4  7093  omxpenlem  9081  setrec2lem1  9955  dfac5lem5  10187  dfac5  10188  kmlem2  10211  kmlem12  10221  kmlem13  10222  initoval  18148  termoval  18149  isinito  18151  istermo  18152  initoid  18156  termoid  18157  initoeu1  18166  initoeu2  18171  termoeu1  18173  upxp  23922  edgnbusgreu  29930  nbusgredgeu0  29931  frgrncvvdeqlem2  30883  bnj852  35534  bnj1489  35669  funpartfv  36679  exeupre  39391  fsuppind  43580  wfac8prim  45944  permac8prim  45956  fourierdlem36  47097  aiotaval  48109  eu2ndop1stv  48139  dfdfat2  48142  tz6.12-afv  48187  tz6.12-afv2  48254  dfatcolem  48269  prprsprreu  48545  prprreueq  48546  initc  50143  initopropd  50295  termopropd  50296  termcterm  50565  termc2  50570