Theorem eubidv 2574

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531  ∃!weu 2556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-mo 2528  df-eu 2557

This theorem is referenced by:  euorv  2600  euanv  2612  reubidva  3380  reueubd  3383  reueq1OLD  3404  eueq2  3703  eueq3  3704  moeq3  3705  reusv2lem2  5398  reusv2lem5  5401  reuhypd  5418  feu  6771  dff3  7107  dff4  7108  omxpenlem  9096  dfac5lem5  10150  dfac5  10151  kmlem2  10174  kmlem12  10184  kmlem13  10185  initoval  17981  termoval  17982  isinito  17984  istermo  17985  initoid  17989  termoid  17990  initoeu1  17999  initoeu2  18004  termoeu1  18006  upxp  23557  edgnbusgreu  29236  nbusgredgeu0  29237  frgrncvvdeqlem2  30166  bnj852  34622  bnj1489  34757  funpartfv  35611  fsuppind  41888  fourierdlem36  45594  aiotaval  46538  eu2ndop1stv  46568  dfdfat2  46571  tz6.12-afv  46616  tz6.12-afv2  46683  dfatcolem  46698  prprsprreu  46922  prprreueq  46923  setrec2lem1  48236