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

Theorem sbcbii 3208
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 11 . . 3  |-  (  T. 
->  ( ph  <->  ps )
)
32sbcbidv 3207 . 2  |-  (  T. 
->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) )
43trud 1332 1  |-  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1325   [.wsbc 3153
This theorem is referenced by:  sbcbiiOLD  3209  eqsbc3r  3210  sbccomlem  3223  sbccom  3224  sbcrext  3226  sbcabel  3230  csbco  3252  sbcnel12g  3260  sbcne12g  3261  sbccsbg  3271  sbccsb2g  3272  csbnestgf  3291  csbabg  3302  sbcss  3730  tfinds2  4835  difopab  4998  mpt2xopovel  6463  2sbcrex  26824  sbcbiiiOLD  26827  sbcrot3  26828  sbcrot5  26829  2rexfrabdioph  26837  3rexfrabdioph  26838  4rexfrabdioph  26839  6rexfrabdioph  26840  7rexfrabdioph  26841  rmydioph  27066  expdiophlem2  27074  sbcrel  27938  sbcfun  27944  bnj62  29012  bnj89  29013  bnj156  29022  bnj524  29032  bnj538  29035  bnj610  29042  bnj919  29063  bnj976  29075  bnj110  29156  bnj91  29159  bnj92  29160  bnj106  29166  bnj121  29168  bnj124  29169  bnj125  29170  bnj126  29171  bnj130  29172  bnj154  29176  bnj155  29177  bnj153  29178  bnj207  29179  bnj523  29185  bnj526  29186  bnj539  29189  bnj540  29190  bnj581  29206  bnj591  29209  bnj609  29215  bnj611  29216  bnj934  29233  bnj1000  29239  bnj985  29251  bnj1040  29268  bnj1123  29282  bnj1463  29351
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-sbc 3154
  Copyright terms: Public domain W3C validator