Theorem sbcimg 3837

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2064   ∈ wcel 2108  [wsbc 3788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789

This theorem is referenced by:  sbcim1OLD  3843  sbceqalOLD  3852  sbc19.21g  3862  sbcssg  4520  iota4an  6543  sbcfung  6590  riotass2  7418  tfinds2  7885  telgsums  20011  bnj110  34872  bnj92  34876  bnj539  34905  bnj540  34906  f1omptsnlem  37337  mptsnunlem  37339  topdifinffinlem  37348  relowlpssretop  37365  rdgeqoa  37371  sbcimi  38117  cdlemkid3N  40935  cdlemkid4  40936  cdlemk35s  40939  cdlemk39s  40941  cdlemk42  40943  frege77  43953  frege116  43992  frege118  43994  sbcim2g  44558  onfrALTlem5  44562  sbcim2gVD  44895  sbcssgVD  44903  onfrALTlem5VD  44905  iccelpart  47420