Theorem eubidv 2583

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃!weu 2565

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 207  df-an 396  df-ex 1781  df-mo 2537  df-eu 2566

This theorem is referenced by:  euorv  2609  euanv  2621  reubidva  3362  reueubd  3365  reueq1OLD  3382  reueqbidv  3386  eueq2  3666  eueq3  3667  moeq3  3668  reusv2lem2  5341  reusv2lem5  5344  reuhypd  5361  feu  6707  dff3  7042  dff4  7043  omxpenlem  9001  dfac5lem5  10028  dfac5  10030  kmlem2  10053  kmlem12  10063  kmlem13  10064  initoval  17910  termoval  17911  isinito  17913  istermo  17914  initoid  17918  termoid  17919  initoeu1  17928  initoeu2  17933  termoeu1  17935  upxp  23548  edgnbusgreu  29356  nbusgredgeu0  29357  frgrncvvdeqlem2  30291  bnj852  34944  bnj1489  35079  funpartfv  36000  exeupre  38513  fsuppind  42698  wfac8prim  45109  permac8prim  45121  fourierdlem36  46255  aiotaval  47209  eu2ndop1stv  47239  dfdfat2  47242  tz6.12-afv  47287  tz6.12-afv2  47354  dfatcolem  47369  prprsprreu  47633  prprreueq  47634  initc  49206  initopropd  49358  termopropd  49359  termcterm  49628  termc2  49633  setrec2lem1  49808