Theorem eubidv 2579

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  ∃!weu 2561

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2533  df-eu 2562

This theorem is referenced by:  euorv  2607  euanv  2619  reubidva  3367  reueubd  3370  reueq1  3390  eueq2  3671  eueq3  3672  moeq3  3673  reusv2lem2  5359  reusv2lem5  5362  reuhypd  5379  feu  6723  dff3  7055  dff4  7056  omxpenlem  9024  dfac5lem5  10072  dfac5  10073  kmlem2  10096  kmlem12  10106  kmlem13  10107  initoval  17893  termoval  17894  isinito  17896  istermo  17897  initoid  17901  termoid  17902  initoeu1  17911  initoeu2  17916  termoeu1  17918  upxp  23011  edgnbusgreu  28378  nbusgredgeu0  28379  frgrncvvdeqlem2  29307  bnj852  33622  bnj1489  33757  funpartfv  34606  fsuppind  40823  fourierdlem36  44504  aiotaval  45447  eu2ndop1stv  45477  dfdfat2  45480  tz6.12-afv  45525  tz6.12-afv2  45592  dfatcolem  45607  prprsprreu  45831  prprreueq  45832  setrec2lem1  47258