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

Theorem sbcan 3768
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 3730 . 2 ([𝐴 / 𝑥](𝜑𝜓) → 𝐴 ∈ V)
2 sbcex 3730 . . 3 ([𝐴 / 𝑥]𝜓𝐴 ∈ V)
32adantl 485 . 2 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) → 𝐴 ∈ V)
4 dfsbcq2 3723 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝐴 / 𝑥](𝜑𝜓)))
5 dfsbcq2 3723 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
6 dfsbcq2 3723 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓[𝐴 / 𝑥]𝜓))
75, 6anbi12d 633 . . 3 (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
8 sban 2085 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
94, 7, 8vtoclbg 3517 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
101, 3, 9pm5.21nii 383 1 ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1538  [wsb 2069  wcel 2111  Vcvv 3441  [wsbc 3720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-sbc 3721
This theorem is referenced by:  sbc3an  3785  sbcabel  3807  2nreu  4349  csbopg  4783  csbuni  4829  csbmpt12  5409  csbxp  5614  difopab  5666  sbcfung  6348  sbcfng  6484  sbcfg  6485  fmptsnd  6908  f1od2  30483  esum2dlem  31461  bnj976  32159  bnj110  32240  bnj1040  32354  csbwrecsg  34744  csboprabg  34747  csbmpo123  34748  f1omptsnlem  34753  mptsnunlem  34755  relowlpssretop  34781  csbfinxpg  34805  sbcani  35546  sbccom2lem  35562  brtrclfv2  40426  cotrclrcl  40441  frege124d  40460  sbiota1  41136  onfrALTlem5  41246  onfrALTlem4  41247  csbingVD  41588  onfrALTlem5VD  41589  onfrALTlem4VD  41590  csbxpgVD  41598  csbunigVD  41602
  Copyright terms: Public domain W3C validator