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 3719	. 2 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ [𝐴 / 𝑥](𝜑 → 𝜓)))
2		dfsbcq2 3719	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3		dfsbcq2 3719	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓))
4	2, 3	imbi12d 345	. 2 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)))
5		sbim 2300	. 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
6	1, 4, 5	vtoclbg 3507	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2067   ∈ wcel 2106  [wsbc 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sbc 3717

This theorem is referenced by:  sbcim1OLD  3773  sbceqalOLD  3783  sbc19.21g  3794  sbcssg  4454  iota4an  6415  sbcfung  6458  riotass2  7263  tfinds2  7710  telgsums  19594  bnj110  32838  bnj92  32842  bnj539  32871  bnj540  32872  f1omptsnlem  35507  mptsnunlem  35509  topdifinffinlem  35518  relowlpssretop  35535  rdgeqoa  35541  sbcimi  36268  cdlemkid3N  38947  cdlemkid4  38948  cdlemk35s  38951  cdlemk39s  38953  cdlemk42  38955  frege77  41548  frege116  41587  frege118  41589  sbcim2g  42158  onfrALTlem5  42162  sbcim2gVD  42495  sbcssgVD  42503  onfrALTlem5VD  42505  iccelpart  44885