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

Theorem sbcan 3370
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 3337 . 2
2 sbcex 3337 . . 3
32adantl 466 . 2
4 dfsbcq2 3330 . . 3
5 dfsbcq2 3330 . . . 4
6 dfsbcq2 3330 . . . 4
75, 6anbi12d 710 . . 3
8 sban 2140 . . 3
94, 7, 8vtoclbg 3168 . 2
101, 3, 9pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  [wsb 1739  e.wcel 1818   cvv 3109  [.wsbc 3327
This theorem is referenced by:  sbc3an  3390  sbcabel  3416  csbuni  4277  csbmpt12  4786  csbxp  5086  difopab  5139  sbcfung  5616  sbcfng  5733  sbcfg  5734  fmptsnd  6093  f1od2  27547  sbcani  30510  sbccom2lem  30529  sbiota1  31341  onfrALTlem5  33314  onfrALTlem4  33315  bnj976  33836  bnj110  33916  bnj1040  34028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-sbc 3328
  Copyright terms: Public domain W3C validator