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

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