Theorem eubidv 2617

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

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

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 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  euorv  2643  euanv  2655  reubidva  3386  reueubd  3389  reueqbidv  3408  eueq2  3676  eueq3  3677  moeq3  3678  reusv2lem2  5375  reusv2lem5  5378  reuhypd  5395  feu  6761  dff3  7102  dff4  7103  omxpenlem  9076  dfac5lem5  10130  dfac5  10131  kmlem2  10154  kmlem12  10164  kmlem13  10165  initoval  18075  termoval  18076  isinito  18078  istermo  18079  initoid  18083  termoid  18084  initoeu1  18093  initoeu2  18098  termoeu1  18100  upxp  23810  edgnbusgreu  29747  nbusgredgeu0  29748  frgrncvvdeqlem2  30681  bnj852  35333  bnj1489  35468  funpartfv  36450  exeupre  39173  fsuppind  43355  wfac8prim  45744  permac8prim  45756  fourierdlem36  46890  aiotaval  47865  eu2ndop1stv  47895  dfdfat2  47898  tz6.12-afv  47943  tz6.12-afv2  48010  dfatcolem  48025  prprsprreu  48301  prprreueq  48302  initc  49902  initopropd  50054  termopropd  50055  termcterm  50324  termc2  50329  setrec2lem1  50504