Theorem sbcbii 3386

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

Syntax hints:   <-> wb 184   T. wtru 1375   [.wsbc 3326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-sbc 3327

This theorem is referenced by:  sbcbiiOLD  3387  eqsbc3r  3388  sbc3an  3389  sbccomlem  3405  sbccom  3406  sbcrextOLD  3408  sbcrext  3409  sbcabel  3415  csbco  3440  sbcnel12g  3821  sbcne12  3822  sbcne12gOLD  3823  csbcom  3832  csbnestgf  3835  sbccsb  3844  sbccsbgOLD  3845  sbccsb2  3846  sbccsb2gOLD  3847  csbab  3850  csbabgOLD  3851  sbcssg  3933  sbcrel  5082  difopab  5127  sbcfung  5604  tfinds2  6671  mpt2xopovel  6940  f1od2  27207  sbcalf  30109  sbcexf  30110  sbccom2lem  30122  sbccom2  30123  sbccom2f  30124  sbccom2fi  30125  csbcom2fi  30127  2sbcrex  30311  2sbcrexOLD  30312  sbcrot3  30317  sbcrot5  30318  2rexfrabdioph  30322  3rexfrabdioph  30323  4rexfrabdioph  30324  6rexfrabdioph  30325  7rexfrabdioph  30326  rmydioph  30551  expdiophlem2  30559  sbc3or  32258  trsbc  32268  onfrALTlem5  32271  bnj62  32730  bnj89  32731  bnj156  32740  bnj524  32750  bnj538  32753  bnj610  32760  bnj919  32781  bnj976  32792  bnj110  32872  bnj91  32875  bnj92  32876  bnj106  32882  bnj121  32884  bnj124  32885  bnj125  32886  bnj126  32887  bnj130  32888  bnj154  32892  bnj155  32893  bnj153  32894  bnj207  32895  bnj523  32901  bnj526  32902  bnj539  32905  bnj540  32906  bnj581  32922  bnj591  32925  bnj609  32931  bnj611  32932  bnj934  32949  bnj1000  32955  bnj984  32966  bnj985  32967  bnj1040  32984  bnj1123  32998  bnj1452  33064  bnj1463  33067