Theorem sbcbii 3491

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

Step	Hyp	Ref	Expression
1		sbcbii.1	. . . 4 |- ( ph <-> ps )
2	1	a1i 11	. . 3 |- ( T. -> ( ph <-> ps ) )
3	2	sbcbidv 3490	. 2 |- ( T. -> ( [. A / x ]. ph <-> [. A / x ]. ps ) )
4	3	trud 1493	1 |- ( [. A / x ]. ph <-> [. A / x ]. ps )

Syntax hints:   <-> wb 196   T. wtru 1484   [.wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436

This theorem is referenced by:  eqsbc3r  3492  eqsbc3rOLD  3493  sbc3an  3494  sbccomlem  3508  sbccom  3509  sbcrext  3511  sbcrextOLD  3512  sbcabel  3517  csbco  3543  sbcnel12g  3985  sbcne12  3986  csbcom  3994  csbnestgf  3996  sbccsb  4004  sbccsb2  4005  csbab  4008  sbcssg  4085  sbcrel  5205  difopab  5253  sbcfung  5912  tfinds2  7063  mpt2xopovel  7346  f1od2  29499  bnj62  30786  bnj89  30787  bnj156  30796  bnj524  30806  bnj538OLD  30810  bnj610  30817  bnj919  30837  bnj976  30848  bnj110  30928  bnj91  30931  bnj92  30932  bnj106  30938  bnj121  30940  bnj124  30941  bnj125  30942  bnj126  30943  bnj130  30944  bnj154  30948  bnj155  30949  bnj153  30950  bnj207  30951  bnj523  30957  bnj526  30958  bnj539  30961  bnj540  30962  bnj581  30978  bnj591  30981  bnj609  30987  bnj611  30988  bnj934  31005  bnj1000  31011  bnj984  31022  bnj985  31023  bnj1040  31040  bnj1123  31054  bnj1452  31120  bnj1463  31123  sbcalf  33917  sbcexf  33918  sbccom2lem  33929  sbccom2  33930  sbccom2f  33931  sbccom2fi  33932  csbcom2fi  33934  2sbcrex  37348  2sbcrexOLD  37350  sbcrot3  37355  sbcrot5  37356  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  rmydioph  37581  expdiophlem2  37589  sbcheg  38073  sbc3or  38738  sbcbiiOLD  38741  trsbc  38750  onfrALTlem5  38757  csbabgOLD  39050