Theorem sbcied 3784

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2714  [wsbc 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3741

This theorem is referenced by:  sbcied2  3785  sbc2ie  3816  sbc2iedv  3817  sbc3ie  3818  sbcralt  3822  csbied  3885  euotd  5461  fmptsnd  7115  riota5f  7343  fpwwe2lem11  10552  fpwwe2lem12  10553  brfi1uzind  14431  opfi1uzind  14434  sbcie3s  17089  issubc  17759  gsumvalx  18601  dmdprd  19929  dprdval  19934  isomnd  20052  issrg  20123  issrng  20777  isorng  20794  islmhm  20979  isphl  21583  istmd  24018  istgp  24021  isnlm  24619  isclm  25020  iscph  25126  iscms  25301  limcfval  25829  ewlksfval  29675  sbcies  32562  abfmpeld  32732  abfmpel  32733  rprmval  33597  f1o2d2  42489