Theorem eubidv 2614

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃!weu 2596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567  df-eu 2597

This theorem is used by:  euorv  2640  euanv  2652  reubidva  3383  reueubd  3386  reueqbidv  3405  eueq2  3671  eueq3  3672  moeq3  3673  reusv2lem2  5365  reusv2lem5  5368  reuhypd  5385  feu  6780  dff3  7124  dff4  7125  omxpenlem  9125  setrec2lem1  10001  dfac5lem5  10233  dfac5  10234  kmlem2  10257  kmlem12  10267  kmlem13  10268  initoval  18197  termoval  18198  isinito  18200  istermo  18201  initoid  18205  termoid  18206  initoeu1  18215  initoeu2  18220  termoeu1  18222  upxp  23972  edgnbusgreu  29978  nbusgredgeu0  29979  frgrncvvdeqlem2  30931  bnj852  35621  bnj1489  35756  funpartfv  36887  exeupre  39615  fsuppind  43811  wfac8prim  46187  permac8prim  46199  fourierdlem36  47358  aiotaval  48370  eu2ndop1stv  48400  dfdfat2  48403  tz6.12-afv  48448  tz6.12-afv2  48515  dfatcolem  48530  prprsprreu  48806  prprreueq  48807  initc  50411  initopropd  50570  termopropd  50571  termcterm  50853  termc2  50858