Theorem sbcied 3773

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 3730	. 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓})
2		sbcied.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		sbcied.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
4	2, 3	elabd3 3614	. 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜒))
5	1, 4	bitrid 283	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730

This theorem is referenced by:  sbcied2  3774  sbc2ie  3805  sbc2iedv  3806  sbc3ie  3807  sbcralt  3811  csbied  3874  euotd  5461  fmptsnd  7117  riota5f  7345  fpwwe2lem11  10555  fpwwe2lem12  10556  brfi1uzind  14461  opfi1uzind  14464  sbcie3s  17123  issubc  17793  gsumvalx  18635  dmdprd  19966  dprdval  19971  isomnd  20089  issrg  20160  issrng  20812  isorng  20829  islmhm  21014  isphl  21618  istmd  24049  istgp  24052  isnlm  24650  isclm  25041  iscph  25147  iscms  25322  limcfval  25849  ewlksfval  29685  sbcies  32572  abfmpeld  32742  abfmpel  32743  rprmval  33591  f1o2d2  42688