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

Theorem sbcbii 3380
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 3379 . 2  |-  ( T. 
->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) )
43trud 1407 1  |-  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1399   [.wsbc 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3325
This theorem is referenced by:  eqsbc3r  3381  sbc3an  3382  sbccomlem  3395  sbccom  3396  sbcrext  3398  sbcabel  3402  csbco  3430  sbcnel12g  3824  sbcne12  3825  csbcom  3833  csbnestgf  3835  sbccsb  3843  sbccsb2  3844  csbab  3847  sbcssg  3928  sbcrel  5077  difopab  5123  sbcfung  5593  tfinds2  6671  mpt2xopovel  6940  f1od2  27778  sbcalf  30757  sbcexf  30758  sbccom2lem  30769  sbccom2  30770  sbccom2f  30771  sbccom2fi  30772  csbcom2fi  30774  2sbcrex  30957  2sbcrexOLD  30959  sbcrot3  30964  sbcrot5  30965  2rexfrabdioph  30969  3rexfrabdioph  30970  4rexfrabdioph  30971  6rexfrabdioph  30972  7rexfrabdioph  30973  rmydioph  31195  expdiophlem2  31203  sbc3or  33689  sbcbiiOLD  33692  trsbc  33701  onfrALTlem5  33708  csbabgOLD  34015  bnj62  34174  bnj89  34175  bnj156  34184  bnj524  34194  bnj538OLD  34198  bnj610  34205  bnj919  34226  bnj976  34237  bnj110  34317  bnj91  34320  bnj92  34321  bnj106  34327  bnj121  34329  bnj124  34330  bnj125  34331  bnj126  34332  bnj130  34333  bnj154  34337  bnj155  34338  bnj153  34339  bnj207  34340  bnj523  34346  bnj526  34347  bnj539  34350  bnj540  34351  bnj581  34367  bnj591  34370  bnj609  34376  bnj611  34377  bnj934  34394  bnj1000  34400  bnj984  34411  bnj985  34412  bnj1040  34429  bnj1123  34443  bnj1452  34509  bnj1463  34512
  Copyright terms: Public domain W3C validator