Theorem sbcied 3765

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1542   ∈ wcel 2110  {cab 2717  [wsbc 3720

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-sbc 3721

This theorem is referenced by:  sbcied2  3767  sbc2ie  3804  sbc2iedv  3806  sbc3ie  3807  sbcralt  3810  csbied  3875  euotd  5431  fmptsnd  7038  riota5f  7257  fpwwe2lem11  10398  fpwwe2lem12  10399  brfi1uzind  14210  opfi1uzind  14213  sbcie3s  16861  issubc  17548  gsumvalx  18358  dmdprd  19599  dprdval  19604  issrg  19741  issrng  20108  islmhm  20287  isphl  20831  isassa  21061  istmd  23223  istgp  23226  isnlm  23837  isclm  24225  iscph  24332  iscms  24507  limcfval  25034  ewlksfval  27966  sbcies  30832  abfmpeld  30987  abfmpel  30988  isomnd  31323  isorng  31494  rprmval  31660