Theorem sbcied 3819

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  {cab 2702  [wsbc 3773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-sbc 3774

This theorem is referenced by:  sbcied2  3821  sbc2ie  3856  sbc2iedv  3858  sbc3ie  3859  sbcralt  3862  csbied  3927  euotd  5515  fmptsnd  7178  riota5f  7404  fpwwe2lem11  10666  fpwwe2lem12  10667  brfi1uzind  14495  opfi1uzind  14498  sbcie3s  17134  issubc  17824  gsumvalx  18639  dmdprd  19967  dprdval  19972  issrg  20140  issrng  20742  islmhm  20924  isphl  21577  istmd  24022  istgp  24025  isnlm  24636  isclm  25035  iscph  25142  iscms  25317  limcfval  25845  ewlksfval  29487  sbcies  32364  abfmpeld  32521  abfmpel  32522  isomnd  32871  isorng  33113  rprmval  33328  f1o2d2  41857