Theorem sbcimg 3773

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  [wsb 2074   ∈ wcel 2121  [wsbc 3725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-sbc 3726

This theorem is referenced by:  sbc19.21g  3796  sbcssg  4452  iota4an  6471  sbcfung  6513  riotass2  7347  tfinds2  7808  telgsums  19963  bnj110  35055  bnj92  35059  bnj539  35088  bnj540  35089  f1omptsnlem  37713  mptsnunlem  37715  topdifinffinlem  37724  relowlpssretop  37741  rdgeqoa  37747  sbcimi  38492  cdlemkid3N  41440  cdlemkid4  41441  cdlemk35s  41444  cdlemk39s  41446  cdlemk42  41448  frege77  44399  frege116  44438  frege118  44440  sbcim2g  44997  onfrALTlem5  45001  sbcim2gVD  45333  sbcssgVD  45341  onfrALTlem5VD  45343  iccelpart  47922