Theorem sbcied 3762

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 1915	. 2 ⊢ Ⅎ𝑥𝜑
4		nfvd 1916	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜒)
5	1, 2, 3, 4	sbciedf 3761	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  [wsbc 3720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-sbc 3721

This theorem is referenced by:  sbcied2  3763  sbc2iedv  3797  sbc3ie  3798  sbcralt  3801  euotd  5368  fmptsnd  6908  riota5f  7121  fpwwe2lem12  10052  fpwwe2lem13  10053  brfi1uzind  13852  opfi1uzind  13855  sbcie3s  16533  issubc  17097  gsumvalx  17878  dmdprd  19113  dprdval  19118  issrg  19250  issrng  19614  islmhm  19792  isphl  20317  isassa  20545  istmd  22679  istgp  22682  isnlm  23281  isclm  23669  iscph  23775  iscms  23949  limcfval  24475  ewlksfval  27391  sbcies  30258  abfmpeld  30417  abfmpel  30418  isomnd  30752  isorng  30923  rprmval  31072