Theorem sbcbii 3010

Description: Formula-building inference 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 9	. . 3 |- ( T. -> ( ph <-> ps ) )
3	2	sbcbidv 3009	. 2 |- ( T. -> ( [. A / x ]. ph <-> [. A / x ]. ps ) )
4	3	mptru 1352	1 |- ( [. A / x ]. ph <-> [. A / x ]. ps )

Syntax hints:   <-> wb 104   T. wtru 1344   [.wsbc 2951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-sbc 2952

This theorem is referenced by:  eqsbc2  3011  sbc3an  3012  sbccomlem  3025  sbccom  3026  sbcabel  3032  csbco  3055  csbcow  3056  sbcnel12g  3062  sbcne12g  3063  sbccsbg  3074  sbccsb2g  3075  csbnestgf  3097  csbabg  3106  sbcssg  3518  sbcrel  4690  difopab  4737  sbcfung  5212  f1od2  6203  mpoxopovel  6209  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlemmain  11931