MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcimg Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 dfsbcq2 3719 . 2 (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝐴 / 𝑥](𝜑𝜓)))
2 dfsbcq2 3719 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
3 dfsbcq2 3719 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓[𝐴 / 𝑥]𝜓))
42, 3imbi12d 345 . 2 (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
5 sbim 2300 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
61, 4, 5vtoclbg 3507 1 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator