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

Theorem sbcan 3843
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 3800 . 2 ([𝐴 / 𝑥](𝜑𝜓) → 𝐴 ∈ V)
2 sbcex 3800 . . 3 ([𝐴 / 𝑥]𝜓𝐴 ∈ V)
32adantl 481 . 2 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) → 𝐴 ∈ V)
4 dfsbcq2 3793 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝐴 / 𝑥](𝜑𝜓)))
5 dfsbcq2 3793 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
6 dfsbcq2 3793 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓[𝐴 / 𝑥]𝜓))
75, 6anbi12d 632 . . 3 (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
8 sban 2077 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
94, 7, 8vtoclbg 3556 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
101, 3, 9pm5.21nii 378 1 ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1536  [wsb 2061  wcel 2105  Vcvv 3477  [wsbc 3790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-sbc 3791
This theorem is referenced by:  sbc3an  3860  sbcabel  3886  2nreu  4449  csbopg  4895  csbuni  4940  csbmpt12  5566  csbxp  5787  difopabOLD  5843  sbcfung  6591  sbcfng  6733  sbcfg  6734  fmptsnd  7188  csbfrecsg  8307  f1od2  32738  esum2dlem  34072  bnj976  34769  bnj110  34850  bnj1040  34964  csboprabg  37312  csbmpo123  37313  f1omptsnlem  37318  mptsnunlem  37320  relowlpssretop  37346  csbfinxpg  37370  sbcani  38094  sbccom2lem  38110  minregex  43523  brtrclfv2  43716  cotrclrcl  43731  frege124d  43750  sbiota1  44429  onfrALTlem5  44539  onfrALTlem4  44540  csbingVD  44881  onfrALTlem5VD  44882  onfrALTlem4VD  44883  csbxpgVD  44891  csbunigVD  44895  rspesbcd  44935
  Copyright terms: Public domain W3C validator