Theorem sbcied 3781

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {cab 2738  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739

This theorem is used by:  sbcied2  3782  sbc2ie  3813  sbc2iedv  3814  sbc3ie  3815  sbcralt  3818  csbied  3882  euotd  5485  fmptsnd  7175  riota5f  7406  mpof1o2d  8140  fpwwe2lem11  10730  fpwwe2lem12  10731  brfi1uzind  14657  opfi1uzind  14660  sbcie3s  17346  issubc  18016  gsumvalx  18871  dmdprd  20220  dprdval  20225  isomnd  20343  issrg  20420  issrng  21107  isorng  21124  islmhm  21308  isphl  21940  istmd  24399  istgp  24402  isnlm  25000  isclm  25391  iscph  25497  iscms  25672  limcfval  26198  ewlksfval  30188  sbcies  33132  abfmpeld  33296  abfmpel  33297  rprmval  34095