Theorem sbcied 3624

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.)

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		sbcied.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		sbcied.2	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
3		nfv 1995	. 2 ⊢ Ⅎ𝑥𝜑
4		nfvd 1996	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜒)
5	1, 2, 3, 4	sbciedf 3623	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  [wsbc 3587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353  df-sbc 3588

This theorem is referenced by:  sbcied2  3625  sbc2iedv  3656  sbc3ie  3657  sbcralt  3660  euotd  5106  fmptsnd  6579  riota5f  6779  fpwwe2lem12  9665  fpwwe2lem13  9666  brfi1uzind  13482  opfi1uzind  13485  sbcie3s  16124  issubc  16702  gsumvalx  17478  dmdprd  18605  dprdval  18610  issrg  18715  issrng  19060  islmhm  19240  isassa  19530  isphl  20190  istmd  22098  istgp  22101  isnlm  22699  isclm  23083  iscph  23189  iscms  23361  limcfval  23856  ewlksfval  26732  sbcies  29662  abfmpeld  29794  abfmpel  29795  isomnd  30041  isorng  30139