Theorem eubidv 2616

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1561  ∃!weu 2598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-mo 2569  df-eu 2599

This theorem is referenced by:  euorv  2642  euanv  2654  reubidva  3384  reueubd  3387  reueqbidv  3406  eueq2  3676  eueq3  3677  moeq3  3678  reusv2lem2  5361  reusv2lem5  5364  reuhypd  5381  feu  6744  dff3  7085  dff4  7086  omxpenlem  9054  dfac5lem5  10099  dfac5  10100  kmlem2  10123  kmlem12  10133  kmlem13  10134  initoval  18040  termoval  18041  isinito  18043  istermo  18044  initoid  18048  termoid  18049  initoeu1  18058  initoeu2  18063  termoeu1  18065  upxp  23741  edgnbusgreu  29626  nbusgredgeu0  29627  frgrncvvdeqlem2  30560  bnj852  35226  bnj1489  35361  funpartfv  36308  exeupre  39002  fsuppind  43184  wfac8prim  45576  permac8prim  45588  fourierdlem36  46715  aiotaval  47687  eu2ndop1stv  47717  dfdfat2  47720  tz6.12-afv  47765  tz6.12-afv2  47832  dfatcolem  47847  prprsprreu  48123  prprreueq  48124  initc  49720  initopropd  49872  termopropd  49873  termcterm  50142  termc2  50147  setrec2lem1  50322