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

Theorem sbcan 3367
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 3334 . 2  |-  ( [. A  /  x ]. ( ph  /\  ps )  ->  A  e.  _V )
2 sbcex 3334 . . 3  |-  ( [. A  /  x ]. ps  ->  A  e.  _V )
32adantl 464 . 2  |-  ( (
[. A  /  x ]. ph  /\  [. A  /  x ]. ps )  ->  A  e.  _V )
4 dfsbcq2 3327 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ( ph  /\  ps )  <->  [. A  /  x ]. ( ph  /\  ps ) ) )
5 dfsbcq2 3327 . . . 4  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
6 dfsbcq2 3327 . . . 4  |-  ( y  =  A  ->  ( [ y  /  x ] ps  <->  [. A  /  x ]. ps ) )
75, 6anbi12d 708 . . 3  |-  ( y  =  A  ->  (
( [ y  /  x ] ph  /\  [
y  /  x ] ps )  <->  ( [. A  /  x ]. ph  /\  [. A  /  x ]. ps ) ) )
8 sban 2142 . . 3  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
94, 7, 8vtoclbg 3165 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ( ph  /\  ps ) 
<->  ( [. A  /  x ]. ph  /\  [. A  /  x ]. ps )
) )
101, 3, 9pm5.21nii 351 1  |-  ( [. A  /  x ]. ( ph  /\  ps )  <->  ( [. A  /  x ]. ph  /\  [. A  /  x ]. ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    = wceq 1398   [wsb 1744    e. wcel 1823   _Vcvv 3106   [.wsbc 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108  df-sbc 3325
This theorem is referenced by:  sbc3an  3382  sbcabel  3402  csbuni  4263  csbmpt12  4770  csbxp  5070  difopab  5123  sbcfung  5593  sbcfng  5710  sbcfg  5711  fmptsnd  6069  f1od2  27781  esum2dlem  28324  sbcani  30753  sbccom2lem  30772  sbiota1  31585  onfrALTlem5  33727  onfrALTlem4  33728  bnj976  34256  bnj110  34336  bnj1040  34448  cotrclrcl  38253  brtrclfv2  38261
  Copyright terms: Public domain W3C validator