Theorem sbcied 3822

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) Avoid ax-10 2138, ax-12 2172. (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 3778	. 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓})
2		sbcied.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		sbcied.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
4	2, 3	elabd3 3661	. 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜒))
5	1, 4	bitrid 283	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  [wsbc 3777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3778

This theorem is referenced by:  sbcied2  3824  sbc2ie  3860  sbc2iedv  3862  sbc3ie  3863  sbcralt  3866  csbied  3931  euotd  5513  fmptsnd  7164  riota5f  7391  fpwwe2lem11  10633  fpwwe2lem12  10634  brfi1uzind  14456  opfi1uzind  14459  sbcie3s  17092  issubc  17782  gsumvalx  18592  dmdprd  19863  dprdval  19868  issrg  20005  issrng  20451  islmhm  20631  isphl  21173  istmd  23570  istgp  23573  isnlm  24184  isclm  24572  iscph  24679  iscms  24854  limcfval  25381  ewlksfval  28848  sbcies  31716  abfmpeld  31867  abfmpel  31868  isomnd  32207  isorng  32406  rprmval  32622  f1o2d2  41053