Theorem sbcied 3773

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2718  [wsbc 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-sbc 3731

This theorem is referenced by:  sbcied2  3774  sbc2ie  3805  sbc2iedv  3806  sbc3ie  3807  sbcralt  3811  csbied  3874  euotd  5461  fmptsnd  7120  riota5f  7348  mpof1o2d  8072  fpwwe2lem11  10562  fpwwe2lem12  10563  brfi1uzind  14468  opfi1uzind  14471  sbcie3s  17130  issubc  17800  gsumvalx  18642  dmdprd  19973  dprdval  19978  isomnd  20096  issrg  20167  issrng  20823  isorng  20840  islmhm  21024  isphl  21610  istmd  24064  istgp  24067  isnlm  24665  isclm  25056  iscph  25162  iscms  25337  limcfval  25864  ewlksfval  29695  sbcies  32582  abfmpeld  32753  abfmpel  32754  rprmval  33606