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

Theorem sbcbii 3218
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 3217 . 2  |-  (  T. 
->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) )
43trud 1333 1  |-  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    T. wtru 1326   [.wsbc 3163
This theorem is referenced by:  sbcbiiOLD  3219  eqsbc3r  3220  sbccomlem  3233  sbccom  3234  sbcrext  3236  sbcabel  3240  csbco  3262  sbcnel12g  3270  sbcne12g  3271  sbccsbg  3281  sbccsb2g  3282  csbnestgf  3301  csbabg  3312  sbcss  3740  tfinds2  4846  difopab  5009  mpt2xopovel  6474  2sbcrex  26857  sbcbiiiOLD  26860  sbcrot3  26861  sbcrot5  26862  2rexfrabdioph  26870  3rexfrabdioph  26871  4rexfrabdioph  26872  6rexfrabdioph  26873  7rexfrabdioph  26874  rmydioph  27099  expdiophlem2  27107  sbcrel  27971  sbcfun  27977  bnj62  29159  bnj89  29160  bnj156  29169  bnj524  29179  bnj538  29182  bnj610  29189  bnj919  29210  bnj976  29222  bnj110  29303  bnj91  29306  bnj92  29307  bnj106  29313  bnj121  29315  bnj124  29316  bnj125  29317  bnj126  29318  bnj130  29319  bnj154  29323  bnj155  29324  bnj153  29325  bnj207  29326  bnj523  29332  bnj526  29333  bnj539  29336  bnj540  29337  bnj581  29353  bnj591  29356  bnj609  29362  bnj611  29363  bnj934  29380  bnj1000  29386  bnj985  29398  bnj1040  29415  bnj1123  29429  bnj1463  29498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-sbc 3164
  Copyright terms: Public domain W3C validator