Theorem sbcbii 3334

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

Syntax hints:   <-> wb 189   T. wtru 1455   [.wsbc 3278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-sbc 3279

This theorem is referenced by:  eqsbc3r  3335  sbc3an  3336  sbccomlem  3349  sbccom  3350  sbcrext  3352  sbcabel  3356  csbco  3384  sbcnel12g  3785  sbcne12  3786  csbcom  3794  csbnestgf  3796  sbccsb  3804  sbccsb2  3805  csbab  3808  sbcssg  3891  sbcrel  4939  difopab  4984  sbcfung  5623  tfinds2  6716  mpt2xopovel  6992  f1od2  28357  bnj62  29574  bnj89  29575  bnj156  29584  bnj524  29594  bnj538OLD  29598  bnj610  29605  bnj919  29626  bnj976  29637  bnj110  29717  bnj91  29720  bnj92  29721  bnj106  29727  bnj121  29729  bnj124  29730  bnj125  29731  bnj126  29732  bnj130  29733  bnj154  29737  bnj155  29738  bnj153  29739  bnj207  29740  bnj523  29746  bnj526  29747  bnj539  29750  bnj540  29751  bnj581  29767  bnj591  29770  bnj609  29776  bnj611  29777  bnj934  29794  bnj1000  29800  bnj984  29811  bnj985  29812  bnj1040  29829  bnj1123  29843  bnj1452  29909  bnj1463  29912  sbcalf  32396  sbcexf  32397  sbccom2lem  32408  sbccom2  32409  sbccom2f  32410  sbccom2fi  32411  csbcom2fi  32413  2sbcrex  35671  2sbcrexOLD  35673  sbcrot3  35678  sbcrot5  35679  2rexfrabdioph  35683  3rexfrabdioph  35684  4rexfrabdioph  35685  6rexfrabdioph  35686  7rexfrabdioph  35687  rmydioph  35913  expdiophlem2  35921  sbcheg  36418  sbc3or  36932  sbcbiiOLD  36935  trsbc  36944  onfrALTlem5  36951  csbabgOLD  37250