Theorem sbcimg 3842

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  [wsb 2061   ∈ wcel 2105  [wsbc 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sbc 3791

This theorem is referenced by:  sbcim1OLD  3848  sbceqalOLD  3857  sbc19.21g  3868  sbcssg  4525  iota4an  6544  sbcfung  6591  riotass2  7417  tfinds2  7884  telgsums  20025  bnj110  34850  bnj92  34854  bnj539  34883  bnj540  34884  f1omptsnlem  37318  mptsnunlem  37320  topdifinffinlem  37329  relowlpssretop  37346  rdgeqoa  37352  sbcimi  38096  cdlemkid3N  40915  cdlemkid4  40916  cdlemk35s  40919  cdlemk39s  40921  cdlemk42  40923  frege77  43929  frege116  43968  frege118  43970  sbcim2g  44535  onfrALTlem5  44539  sbcim2gVD  44872  sbcssgVD  44880  onfrALTlem5VD  44882  iccelpart  47357