Theorem sbcied 3762

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {cab 2716  [wsbc 3717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-sbc 3718

This theorem is referenced by:  sbcied2  3764  sbc2ie  3800  sbc2iedv  3802  sbc3ie  3803  sbcralt  3806  csbied  3871  euotd  5428  fmptsnd  7050  riota5f  7270  fpwwe2lem11  10406  fpwwe2lem12  10407  brfi1uzind  14221  opfi1uzind  14224  sbcie3s  16872  issubc  17559  gsumvalx  18369  dmdprd  19610  dprdval  19615  issrg  19752  issrng  20119  islmhm  20298  isphl  20842  isassa  21072  istmd  23234  istgp  23237  isnlm  23848  isclm  24236  iscph  24343  iscms  24518  limcfval  25045  ewlksfval  27977  sbcies  30845  abfmpeld  31000  abfmpel  31001  isomnd  31336  isorng  31507  rprmval  31673