Theorem sbcied 3836

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {cab 2711  [wsbc 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sbc 3791

This theorem is referenced by:  sbcied2  3838  sbc2ie  3873  sbc2iedv  3875  sbc3ie  3876  sbcralt  3880  csbied  3945  euotd  5522  fmptsnd  7188  riota5f  7415  fpwwe2lem11  10678  fpwwe2lem12  10679  brfi1uzind  14543  opfi1uzind  14546  sbcie3s  17195  issubc  17885  gsumvalx  18701  dmdprd  20032  dprdval  20037  issrg  20205  issrng  20861  islmhm  21043  isphl  21663  istmd  24097  istgp  24100  isnlm  24711  isclm  25110  iscph  25217  iscms  25392  limcfval  25921  ewlksfval  29633  sbcies  32515  abfmpeld  32670  abfmpel  32671  isomnd  33060  isorng  33308  rprmval  33523  f1o2d2  42252