Theorem sbcied 3794

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {cab 2747  [wsbc 3751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sbc 3752

This theorem is referenced by:  sbcied2  3795  sbc2ie  3826  sbc2iedv  3827  sbc3ie  3828  sbcralt  3832  csbied  3895  euotd  5497  fmptsnd  7168  riota5f  7396  mpof1o2d  8121  fpwwe2lem11  10626  fpwwe2lem12  10627  brfi1uzind  14545  opfi1uzind  14548  sbcie3s  17222  issubc  17892  gsumvalx  18734  dmdprd  20070  dprdval  20075  isomnd  20193  issrg  20270  issrng  20925  isorng  20942  islmhm  21126  isphl  21747  istmd  24200  istgp  24203  isnlm  24801  isclm  25192  iscph  25298  iscms  25473  limcfval  26000  ewlksfval  29892  sbcies  32775  abfmpeld  32940  abfmpel  32941  rprmval  33751