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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1566  ∃!weu 2594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-mo 2565  df-eu 2595

This theorem is referenced by:  euorv  2638  euanv  2650  reubidva  3381  reueubd  3384  reueqbidv  3403  eueq2  3672  eueq3  3673  moeq3  3674  reusv2lem2  5370  reusv2lem5  5373  reuhypd  5390  feu  6754  dff3  7095  dff4  7096  omxpenlem  9065  dfac5lem5  10110  dfac5  10111  kmlem2  10134  kmlem12  10144  kmlem13  10145  initoval  18049  termoval  18050  isinito  18052  istermo  18053  initoid  18057  termoid  18058  initoeu1  18067  initoeu2  18072  termoeu1  18074  upxp  23759  edgnbusgreu  29683  nbusgredgeu0  29684  frgrncvvdeqlem2  30617  bnj852  35275  bnj1489  35410  funpartfv  36403  exeupre  39108  fsuppind  43292  wfac8prim  45681  permac8prim  45693  fourierdlem36  46827  aiotaval  47799  eu2ndop1stv  47829  dfdfat2  47832  tz6.12-afv  47877  tz6.12-afv2  47944  dfatcolem  47959  prprsprreu  48235  prprreueq  48236  initc  49836  initopropd  49988  termopropd  49989  termcterm  50258  termc2  50263  setrec2lem1  50438