Theorem eubidv 2672

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535  ∃!weu 2653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622  df-eu 2654

This theorem is referenced by:  euorv  2696  euanv  2709  reubidva  3390  reueq1  3409  reueubd  3438  eueq2  3703  eueq3  3704  moeq3  3705  reusv2lem2  5302  reusv2lem5  5305  reuhypd  5322  feu  6556  dff3  6868  dff4  6869  omxpenlem  8620  dfac5lem5  9555  dfac5  9556  kmlem2  9579  kmlem12  9589  kmlem13  9590  initoval  17259  termoval  17260  isinito  17262  istermo  17263  initoid  17267  termoid  17268  initoeu1  17273  initoeu2  17278  termoeu1  17280  upxp  22233  edgnbusgreu  27151  nbusgredgeu0  27152  frgrncvvdeqlem2  28081  bnj852  32195  bnj1489  32330  funpartfv  33408  fourierdlem36  42435  aiotaval  43300  eu2ndop1stv  43331  dfdfat2  43334  tz6.12-afv  43379  tz6.12-afv2  43446  dfatcolem  43461  prprsprreu  43688  prprreueq  43689  setrec2lem1  44803