Theorem sbcied 3756

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) Avoid ax-10 2139, ax-12 2173. (Revised by Gino Giotto, 12-Oct-2024.)

Hypotheses

Ref	Expression
sbcied.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sbcied.2	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
sbcied	⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem sbcied

Step	Hyp	Ref	Expression
1		df-sbc 3712	. 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓})
2		sbcied.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		sbcied.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
4	2, 3	elabd3 3595	. 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜒))
5	1, 4	syl5bb 282	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {cab 2715  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712

This theorem is referenced by:  sbcied2  3758  sbc2ie  3795  sbc2iedv  3797  sbc3ie  3798  sbcralt  3801  csbied  3866  euotd  5421  fmptsnd  7023  riota5f  7241  fpwwe2lem11  10328  fpwwe2lem12  10329  brfi1uzind  14140  opfi1uzind  14143  sbcie3s  16791  issubc  17466  gsumvalx  18275  dmdprd  19516  dprdval  19521  issrg  19658  issrng  20025  islmhm  20204  isphl  20745  isassa  20973  istmd  23133  istgp  23136  isnlm  23745  isclm  24133  iscph  24239  iscms  24414  limcfval  24941  ewlksfval  27871  sbcies  30737  abfmpeld  30893  abfmpel  30894  isomnd  31229  isorng  31400  rprmval  31566