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

Theorem sbcbii 3046
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 3045 . 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 2991
This theorem is referenced by:  sbcbiiOLD  3047  eqsbc3r  3048  sbccomlem  3061  sbccom  3062  sbcrext  3064  sbcabel  3068  csbco  3090  sbcnel12g  3098  sbcne12g  3099  sbccsbg  3109  sbccsb2g  3110  csbnestgf  3129  csbabg  3142  sbcss  3564  tfinds2  4654  difopab  4817  bisig0  26062  sbcbiiiOLD  26867  sbcrot3  26868  sbcrot5  26869  sbcrel  27979  sbcfun  27985  mpt2xopovel  28086  bnj62  28746  bnj156  28756  bnj610  28776  bnj976  28809  bnj110  28890  bnj124  28903  bnj154  28910  bnj155  28911  bnj153  28912  bnj581  28940  bnj591  28943  bnj609  28949  bnj985  28985  bnj1040  29002  bnj1123  29016  bnj1463  29085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992
  Copyright terms: Public domain W3C validator