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

Theorem sbcbii 3059
Description: Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.)
Hypothesis
Ref Expression
sbcbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
sbcbii  |-  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps )

Proof of Theorem sbcbii
StepHypRef Expression
1 sbcbii.1 . . . 4  |-  ( ph  <->  ps )
21a1i 10 . . 3  |-  (  T. 
->  ( ph  <->  ps )
)
32sbcbidv 3058 . 2  |-  (  T. 
->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) )
43trud 1314 1  |-  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    T. wtru 1307   [.wsbc 3004
This theorem is referenced by:  sbcbiiOLD  3060  eqsbc3r  3061  sbccomlem  3074  sbccom  3075  sbcrext  3077  sbcabel  3081  csbco  3103  sbcnel12g  3111  sbcne12g  3112  sbccsbg  3122  sbccsb2g  3123  csbnestgf  3142  csbabg  3155  sbcss  3577  tfinds2  4670  difopab  4833  bisig0  26165  sbcbiiiOLD  26970  sbcrot3  26971  sbcrot5  26972  sbcrel  28084  sbcfun  28090  mpt2xopovel  28202  bnj62  29062  bnj156  29072  bnj610  29092  bnj976  29125  bnj110  29206  bnj124  29219  bnj154  29226  bnj155  29227  bnj153  29228  bnj581  29256  bnj591  29259  bnj609  29265  bnj985  29301  bnj1040  29318  bnj1123  29332  bnj1463  29401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-sbc 3005
  Copyright terms: Public domain W3C validator