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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  ∃!weu 2561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-eu 2562

This theorem is referenced by:  euorv  2605  euanv  2617  reubidva  3370  reueubd  3373  reueq1OLD  3390  reueqbidv  3394  eueq2  3681  eueq3  3682  moeq3  3683  reusv2lem2  5354  reusv2lem5  5357  reuhypd  5374  feu  6736  dff3  7072  dff4  7073  omxpenlem  9042  dfac5lem5  10080  dfac5  10082  kmlem2  10105  kmlem12  10115  kmlem13  10116  initoval  17955  termoval  17956  isinito  17958  istermo  17959  initoid  17963  termoid  17964  initoeu1  17973  initoeu2  17978  termoeu1  17980  upxp  23510  edgnbusgreu  29294  nbusgredgeu0  29295  frgrncvvdeqlem2  30229  bnj852  34911  bnj1489  35046  funpartfv  35933  fsuppind  42578  wfac8prim  44992  permac8prim  45004  fourierdlem36  46141  aiotaval  47096  eu2ndop1stv  47126  dfdfat2  47129  tz6.12-afv  47174  tz6.12-afv2  47241  dfatcolem  47256  prprsprreu  47520  prprreueq  47521  initc  49080  initopropd  49232  termopropd  49233  termcterm  49502  termc2  49507  setrec2lem1  49682