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

Theorem sbcan 3830
Description: Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.)
Assertion
Ref Expression
sbcan ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))

Proof of Theorem sbcan
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 sbcex 3788 . 2 ([𝐴 / 𝑥](𝜑𝜓) → 𝐴 ∈ V)
2 sbcex 3788 . . 3 ([𝐴 / 𝑥]𝜓𝐴 ∈ V)
32adantl 483 . 2 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) → 𝐴 ∈ V)
4 dfsbcq2 3781 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝐴 / 𝑥](𝜑𝜓)))
5 dfsbcq2 3781 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
6 dfsbcq2 3781 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓[𝐴 / 𝑥]𝜓))
75, 6anbi12d 632 . . 3 (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
8 sban 2084 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
94, 7, 8vtoclbg 3560 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
101, 3, 9pm5.21nii 380 1 ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  [wsb 2068  wcel 2107  Vcvv 3475  [wsbc 3778
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sbc 3779
This theorem is referenced by:  sbc3an  3848  sbcabel  3873  2nreu  4442  csbopg  4892  csbuni  4941  csbmpt12  5558  csbxp  5776  difopabOLD  5832  sbcfung  6573  sbcfng  6715  sbcfg  6716  fmptsnd  7167  csbfrecsg  8269  f1od2  31977  esum2dlem  33121  bnj976  33819  bnj110  33900  bnj1040  34014  csboprabg  36259  csbmpo123  36260  f1omptsnlem  36265  mptsnunlem  36267  relowlpssretop  36293  csbfinxpg  36317  sbcani  37024  sbccom2lem  37040  minregex  42333  brtrclfv2  42526  cotrclrcl  42541  frege124d  42560  sbiota1  43241  onfrALTlem5  43351  onfrALTlem4  43352  csbingVD  43693  onfrALTlem5VD  43694  onfrALTlem4VD  43695  csbxpgVD  43703  csbunigVD  43707
  Copyright terms: Public domain W3C validator