Theorem eubidv 2589

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  ∃!weu 2571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543  df-eu 2572

This theorem is referenced by:  euorv  2615  euanv  2627  reubidva  3404  reueubd  3407  reueq1OLD  3428  eueq2  3732  eueq3  3733  moeq3  3734  reusv2lem2  5417  reusv2lem5  5420  reuhypd  5437  feu  6797  dff3  7134  dff4  7135  omxpenlem  9139  dfac5lem5  10196  dfac5  10198  kmlem2  10221  kmlem12  10231  kmlem13  10232  initoval  18060  termoval  18061  isinito  18063  istermo  18064  initoid  18068  termoid  18069  initoeu1  18078  initoeu2  18083  termoeu1  18085  upxp  23652  edgnbusgreu  29402  nbusgredgeu0  29403  frgrncvvdeqlem2  30332  bnj852  34897  bnj1489  35032  funpartfv  35909  reueqbidv  36179  fsuppind  42545  fourierdlem36  46064  aiotaval  47010  eu2ndop1stv  47040  dfdfat2  47043  tz6.12-afv  47088  tz6.12-afv2  47155  dfatcolem  47170  prprsprreu  47393  prprreueq  47394  setrec2lem1  48785