Theorem sbcbii 3344

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

Syntax hints:   <-> wb 184   T. wtru 1371   [.wsbc 3284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-sbc 3285

This theorem is referenced by:  sbcbiiOLD  3345  eqsbc3r  3346  sbc3an  3347  sbccomlem  3363  sbccom  3364  sbcrextOLD  3366  sbcrext  3367  sbcabel  3373  csbco  3396  sbcnel12g  3776  sbcne12  3777  sbcne12gOLD  3778  csbcom  3787  csbnestgf  3790  sbccsb  3799  sbccsbgOLD  3800  sbccsb2  3801  sbccsb2gOLD  3802  csbab  3805  csbabgOLD  3806  sbcssg  3888  sbcrel  5024  difopab  5069  sbcfung  5539  tfinds2  6574  mpt2xopovel  6837  f1od2  26158  sbcalf  29058  sbcexf  29059  sbccom2lem  29071  sbccom2  29072  sbccom2f  29073  sbccom2fi  29074  csbcom2fi  29076  2sbcrex  29261  2sbcrexOLD  29262  sbcrot3  29267  sbcrot5  29268  2rexfrabdioph  29272  3rexfrabdioph  29273  4rexfrabdioph  29274  6rexfrabdioph  29275  7rexfrabdioph  29276  rmydioph  29501  expdiophlem2  29509  sbc3or  31537  trsbc  31547  onfrALTlem5  31550  bnj62  32009  bnj89  32010  bnj156  32019  bnj524  32029  bnj538  32032  bnj610  32039  bnj919  32060  bnj976  32071  bnj110  32151  bnj91  32154  bnj92  32155  bnj106  32161  bnj121  32163  bnj124  32164  bnj125  32165  bnj126  32166  bnj130  32167  bnj154  32171  bnj155  32172  bnj153  32173  bnj207  32174  bnj523  32180  bnj526  32181  bnj539  32184  bnj540  32185  bnj581  32201  bnj591  32204  bnj609  32210  bnj611  32211  bnj934  32228  bnj1000  32234  bnj984  32245  bnj985  32246  bnj1040  32263  bnj1123  32277  bnj1452  32343  bnj1463  32346