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

Theorem sbcan 3838
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 3798 . 2 ([𝐴 / 𝑥](𝜑𝜓) → 𝐴 ∈ V)
2 sbcex 3798 . . 3 ([𝐴 / 𝑥]𝜓𝐴 ∈ V)
32adantl 481 . 2 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) → 𝐴 ∈ V)
4 dfsbcq2 3791 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝐴 / 𝑥](𝜑𝜓)))
5 dfsbcq2 3791 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
6 dfsbcq2 3791 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓[𝐴 / 𝑥]𝜓))
75, 6anbi12d 632 . . 3 (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
8 sban 2080 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
94, 7, 8vtoclbg 3557 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
101, 3, 9pm5.21nii 378 1 ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  [wsb 2064  wcel 2108  Vcvv 3480  [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-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-sbc 3789
This theorem is referenced by:  sbc3an  3855  sbcabel  3878  2nreu  4444  csbopg  4891  csbuni  4936  csbmpt12  5562  csbxp  5785  difopabOLD  5841  sbcfung  6590  sbcfng  6733  sbcfg  6734  fmptsnd  7189  csbfrecsg  8309  f1od2  32732  esum2dlem  34093  bnj976  34791  bnj110  34872  bnj1040  34986  csboprabg  37331  csbmpo123  37332  f1omptsnlem  37337  mptsnunlem  37339  relowlpssretop  37365  csbfinxpg  37389  sbcani  38115  sbccom2lem  38131  minregex  43547  brtrclfv2  43740  cotrclrcl  43755  frege124d  43774  sbiota1  44453  onfrALTlem5  44562  onfrALTlem4  44563  csbingVD  44904  onfrALTlem5VD  44905  onfrALTlem4VD  44906  csbxpgVD  44914  csbunigVD  44918  rspesbcd  44958
  Copyright terms: Public domain W3C validator