Theorem eubidv 2587

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃!weu 2569

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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570

This theorem is referenced by:  euorv  2613  euanv  2625  reubidva  3365  reueubd  3368  reueq1OLD  3385  reueqbidv  3389  eueq2  3669  eueq3  3670  moeq3  3671  reusv2lem2  5345  reusv2lem5  5348  reuhypd  5365  feu  6711  dff3  7047  dff4  7048  omxpenlem  9010  dfac5lem5  10041  dfac5  10043  kmlem2  10066  kmlem12  10076  kmlem13  10077  initoval  17921  termoval  17922  isinito  17924  istermo  17925  initoid  17929  termoid  17930  initoeu1  17939  initoeu2  17944  termoeu1  17946  upxp  23571  edgnbusgreu  29423  nbusgredgeu0  29424  frgrncvvdeqlem2  30358  bnj852  35058  bnj1489  35193  funpartfv  36120  exeupre  38663  fsuppind  42869  wfac8prim  45279  permac8prim  45291  fourierdlem36  46423  aiotaval  47377  eu2ndop1stv  47407  dfdfat2  47410  tz6.12-afv  47455  tz6.12-afv2  47522  dfatcolem  47537  prprsprreu  47801  prprreueq  47802  initc  49372  initopropd  49524  termopropd  49525  termcterm  49794  termc2  49799  setrec2lem1  49974