Theorem sbiev 2308

Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2501 with a disjoint variable condition, not requiring ax-13 2371. See sbievw 2095 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2137 and shorten proof. (Revised by BJ, 18-Jul-2023.)

Hypotheses

Ref	Expression
sbiev.1	⊢ Ⅎ𝑥𝜓
sbiev.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbiev	⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbiev

Step	Hyp	Ref	Expression
1		sb6 2088	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		sbiev.1	. . 3 ⊢ Ⅎ𝑥𝜓
3		sbiev.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	equsalv 2258	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
5	1, 4	bitri 274	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  Ⅎwnf 1785  [wsb 2067

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-sb 2068

This theorem is referenced by:  sbiedw  2309  sbco2v  2326  mo4f  2561  cbvmowOLD  2598  cbveuwOLD  2602  cbvabwOLD  2807  cbvralfwOLD  3320  cbvreuwOLD  3412  cbvrabw  3467  reu2  3720  rmo4f  3730  sbcralt  3865  sbcreu  3869  sbcel12  4407  sbceqg  4408  sbcbr123  5201  cbvmptf  5256  frpoins2fg  6342  wfis2fgOLD  6355  tfis2f  7841  tfinds  7845  frins2f  9744  clwwlknonclwlknonf1o  29604  dlwwlknondlwlknonf1o  29607  funcnv4mpt  31881  nn0min  32013  ballotlemodife  33484  bnj1321  34026  setinds2f  34739  bj-sbeqALT  35768  scottabf  42984