Theorem sbcied 3689

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2107  [wsbc 3652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-v 3400  df-sbc 3653

This theorem is referenced by:  sbcied2  3690  sbc2iedv  3724  sbc3ie  3725  sbcralt  3728  euotd  5210  fmptsnd  6702  riota5f  6908  fpwwe2lem12  9798  fpwwe2lem13  9799  brfi1uzind  13594  opfi1uzind  13597  sbcie3s  16313  issubc  16880  gsumvalx  17656  dmdprd  18784  dprdval  18789  issrg  18894  issrng  19242  islmhm  19422  isassa  19712  isphl  20371  istmd  22286  istgp  22289  isnlm  22887  isclm  23271  iscph  23377  iscms  23551  limcfval  24073  ewlksfval  26949  sbcies  29894  abfmpeld  30019  abfmpel  30020  isomnd  30263  isorng  30361