Theorem eubidv 2613

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-mo 2566  df-eu 2596

This theorem is used by:  euorv  2639  euanv  2651  reubidva  3382  reueubd  3385  reueqbidv  3404  eueq2  3672  eueq3  3673  moeq3  3674  reusv2lem2  5369  reusv2lem5  5372  reuhypd  5389  feu  6754  dff3  7095  dff4  7096  omxpenlem  9064  dfac5lem5  10118  dfac5  10119  kmlem2  10142  kmlem12  10152  kmlem13  10153  initoval  18056  termoval  18057  isinito  18059  istermo  18060  initoid  18064  termoid  18065  initoeu1  18074  initoeu2  18079  termoeu1  18081  upxp  23791  edgnbusgreu  29728  nbusgredgeu0  29729  frgrncvvdeqlem2  30662  bnj852  35318  bnj1489  35453  funpartfv  36445  exeupre  39168  fsuppind  43350  wfac8prim  45739  permac8prim  45751  fourierdlem36  46885  aiotaval  47860  eu2ndop1stv  47890  dfdfat2  47893  tz6.12-afv  47938  tz6.12-afv2  48005  dfatcolem  48020  prprsprreu  48296  prprreueq  48297  initc  49897  initopropd  50049  termopropd  50050  termcterm  50319  termc2  50324  setrec2lem1  50499