Theorem sbcied 3439

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  [wsbc 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-sbc 3403

This theorem is referenced by:  sbcied2  3440  sbc2iedv  3473  sbc3ie  3474  sbcralt  3477  euotd  4900  fmptsnd  6340  riota5f  6535  fpwwe2lem12  9342  fpwwe2lem13  9343  brfi1uzind  13135  opfi1uzind  13138  brfi1uzindOLD  13141  opfi1uzindOLD  13144  sbcie3s  15745  issubc  16318  gsumvalx  17093  dmdprd  18220  dprdval  18225  issrg  18330  issrng  18673  islmhm  18848  isassa  19136  isphl  19792  istmd  21688  istgp  21691  isnlm  22289  isclm  22672  iscph  22778  iscms  22950  limcfval  23442  sbcies  28706  abfmpeld  28834  abfmpel  28835  isomnd  29032  isorng  29130  ewlksfval  40803