Theorem sbcbii 3356

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 3355	. 2 |- ( T. -> ( [. A / x ]. ph <-> [. A / x ]. ps ) )
4	3	trud 1447	1 |- ( [. A / x ]. ph <-> [. A / x ]. ps )

Syntax hints:   <-> wb 188   T. wtru 1439   [.wsbc 3300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-sbc 3301

This theorem is referenced by:  eqsbc3r  3357  sbc3an  3358  sbccomlem  3371  sbccom  3372  sbcrext  3374  sbcabel  3378  csbco  3406  sbcnel12g  3803  sbcne12  3804  csbcom  3812  csbnestgf  3814  sbccsb  3822  sbccsb2  3823  csbab  3826  sbcssg  3909  sbcrel  4938  difopab  4983  sbcfung  5622  tfinds2  6702  mpt2xopovel  6972  f1od2  28309  bnj62  29528  bnj89  29529  bnj156  29538  bnj524  29548  bnj538OLD  29552  bnj610  29559  bnj919  29580  bnj976  29591  bnj110  29671  bnj91  29674  bnj92  29675  bnj106  29681  bnj121  29683  bnj124  29684  bnj125  29685  bnj126  29686  bnj130  29687  bnj154  29691  bnj155  29692  bnj153  29693  bnj207  29694  bnj523  29700  bnj526  29701  bnj539  29704  bnj540  29705  bnj581  29721  bnj591  29724  bnj609  29730  bnj611  29731  bnj934  29748  bnj1000  29754  bnj984  29765  bnj985  29766  bnj1040  29783  bnj1123  29797  bnj1452  29863  bnj1463  29866  sbcalf  32310  sbcexf  32311  sbccom2lem  32322  sbccom2  32323  sbccom2f  32324  sbccom2fi  32325  csbcom2fi  32327  2sbcrex  35590  2sbcrexOLD  35592  sbcrot3  35597  sbcrot5  35598  2rexfrabdioph  35602  3rexfrabdioph  35603  4rexfrabdioph  35604  6rexfrabdioph  35605  7rexfrabdioph  35606  rmydioph  35833  expdiophlem2  35841  sbcheg  36276  sbc3or  36791  sbcbiiOLD  36794  trsbc  36803  onfrALTlem5  36810  csbabgOLD  37116