Theorem sbcimg 3767

Description: Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.)

Assertion

Ref	Expression
sbcimg	⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)))

Proof of Theorem sbcimg

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3723	. 2 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ [𝐴 / 𝑥](𝜑 → 𝜓)))
2		dfsbcq2 3723	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3		dfsbcq2 3723	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓))
4	2, 3	imbi12d 348	. 2 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)))
5		sbim 2307	. 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
6	1, 4, 5	vtoclbg 3517	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  [wsb 2069   ∈ 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-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3721

This theorem is referenced by:  sbcim1  3772  sbceqal  3782  sbc19.21g  3792  sbcssg  4421  iota4an  6306  sbcfung  6348  riotass2  7123  tfinds2  7558  telgsums  19106  bnj110  32240  bnj92  32244  bnj539  32273  bnj540  32274  f1omptsnlem  34753  mptsnunlem  34755  topdifinffinlem  34764  relowlpssretop  34781  rdgeqoa  34787  sbcimi  35548  cdlemkid3N  38229  cdlemkid4  38230  cdlemk35s  38233  cdlemk39s  38235  cdlemk42  38237  frege77  40641  frege116  40680  frege118  40682  sbcim2g  41244  onfrALTlem5  41248  sbcim2gVD  41581  sbcssgVD  41589  onfrALTlem5VD  41591  iccelpart  43950