Theorem sbcied 3772

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2714  [wsbc 3728

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3729

This theorem is referenced by:  sbcied2  3773  sbc2ie  3804  sbc2iedv  3805  sbc3ie  3806  sbcralt  3810  csbied  3873  euotd  5467  fmptsnd  7124  riota5f  7352  fpwwe2lem11  10564  fpwwe2lem12  10565  brfi1uzind  14470  opfi1uzind  14473  sbcie3s  17132  issubc  17802  gsumvalx  18644  dmdprd  19975  dprdval  19980  isomnd  20098  issrg  20169  issrng  20821  isorng  20838  islmhm  21022  isphl  21608  istmd  24039  istgp  24042  isnlm  24640  isclm  25031  iscph  25137  iscms  25312  limcfval  25839  ewlksfval  29670  sbcies  32557  abfmpeld  32727  abfmpel  32728  rprmval  33576  f1o2d2  42674