Theorem eubidv 2587

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃!weu 2569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570

This theorem is referenced by:  euorv  2613  euanv  2625  reubidva  3366  reueubd  3369  reueq1OLD  3386  reueqbidv  3390  eueq2  3670  eueq3  3671  moeq3  3672  reusv2lem2  5346  reusv2lem5  5349  reuhypd  5366  feu  6718  dff3  7054  dff4  7055  omxpenlem  9018  dfac5lem5  10049  dfac5  10051  kmlem2  10074  kmlem12  10084  kmlem13  10085  initoval  17929  termoval  17930  isinito  17932  istermo  17933  initoid  17937  termoid  17938  initoeu1  17947  initoeu2  17952  termoeu1  17954  upxp  23579  edgnbusgreu  29452  nbusgredgeu0  29453  frgrncvvdeqlem2  30387  bnj852  35096  bnj1489  35231  funpartfv  36158  exeupre  38731  fsuppind  42937  wfac8prim  45347  permac8prim  45359  fourierdlem36  46490  aiotaval  47444  eu2ndop1stv  47474  dfdfat2  47477  tz6.12-afv  47522  tz6.12-afv2  47589  dfatcolem  47604  prprsprreu  47868  prprreueq  47869  initc  49439  initopropd  49591  termopropd  49592  termcterm  49861  termc2  49866  setrec2lem1  50041