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

Theorem sbcan 3321
Description: Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.)
Assertion
Ref Expression
sbcan  |-  ( [. A  /  x ]. ( ph  /\  ps )  <->  ( [. A  /  x ]. ph  /\  [. A  /  x ]. ps ) )

Proof of Theorem sbcan
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 sbcex 3288 . 2  |-  ( [. A  /  x ]. ( ph  /\  ps )  ->  A  e.  _V )
2 sbcex 3288 . . 3  |-  ( [. A  /  x ]. ps  ->  A  e.  _V )
32adantl 472 . 2  |-  ( (
[. A  /  x ]. ph  /\  [. A  /  x ]. ps )  ->  A  e.  _V )
4 dfsbcq2 3281 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ( ph  /\  ps )  <->  [. A  /  x ]. ( ph  /\  ps ) ) )
5 dfsbcq2 3281 . . . 4  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
6 dfsbcq2 3281 . . . 4  |-  ( y  =  A  ->  ( [ y  /  x ] ps  <->  [. A  /  x ]. ps ) )
75, 6anbi12d 722 . . 3  |-  ( y  =  A  ->  (
( [ y  /  x ] ph  /\  [
y  /  x ] ps )  <->  ( [. A  /  x ]. ph  /\  [. A  /  x ]. ps ) ) )
8 sban 2238 . . 3  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
94, 7, 8vtoclbg 3119 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ( ph  /\  ps ) 
<->  ( [. A  /  x ]. ph  /\  [. A  /  x ]. ps )
) )
101, 3, 9pm5.21nii 359 1  |-  ( [. A  /  x ]. ( ph  /\  ps )  <->  ( [. A  /  x ]. ph  /\  [. A  /  x ]. ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375    = wceq 1454   [wsb 1807    e. wcel 1897   _Vcvv 3056   [.wsbc 3278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058  df-sbc 3279
This theorem is referenced by:  sbc3an  3336  sbcabel  3356  csbuni  4239  csbmpt12  4748  csbxp  4934  difopab  4984  sbcfung  5623  sbcfng  5747  sbcfg  5748  fmptsnd  6109  f1od2  28357  esum2dlem  28961  bnj976  29637  bnj110  29717  bnj1040  29829  csbopg2  31769  csbwrecsg  31772  csboprabg  31775  csbmpt22g  31776  f1omptsnlem  31782  mptsnunlem  31784  relowlpssretop  31811  csbfinxpg  31824  sbcani  32389  sbccom2lem  32408  brtrclfv2  36363  cotrclrcl  36378  frege124d  36397  sbiota1  36828  onfrALTlem5  36951  onfrALTlem4  36952
  Copyright terms: Public domain W3C validator