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

Theorem sbcbii 3160
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 3159 . 2  |-  (  T. 
->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) )
43trud 1329 1  |-  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1322   [.wsbc 3105
This theorem is referenced by:  sbcbiiOLD  3161  eqsbc3r  3162  sbccomlem  3175  sbccom  3176  sbcrext  3178  sbcabel  3182  csbco  3204  sbcnel12g  3212  sbcne12g  3213  sbccsbg  3223  sbccsb2g  3224  csbnestgf  3243  csbabg  3254  sbcss  3682  tfinds2  4784  difopab  4947  mpt2xopovel  6408  2sbcrex  26535  sbcbiiiOLD  26538  sbcrot3  26539  sbcrot5  26540  2rexfrabdioph  26548  3rexfrabdioph  26549  4rexfrabdioph  26550  6rexfrabdioph  26551  7rexfrabdioph  26552  rmydioph  26777  expdiophlem2  26785  sbcrel  27650  sbcfun  27656  bnj62  28424  bnj89  28425  bnj156  28434  bnj524  28444  bnj538  28447  bnj610  28454  bnj919  28475  bnj976  28487  bnj110  28568  bnj91  28571  bnj92  28572  bnj106  28578  bnj121  28580  bnj124  28581  bnj125  28582  bnj126  28583  bnj130  28584  bnj154  28588  bnj155  28589  bnj153  28590  bnj207  28591  bnj523  28597  bnj526  28598  bnj539  28601  bnj540  28602  bnj581  28618  bnj591  28621  bnj609  28627  bnj611  28628  bnj934  28645  bnj1000  28651  bnj985  28663  bnj1040  28680  bnj1123  28694  bnj1463  28763
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-sbc 3106
  Copyright terms: Public domain W3C validator