Theorem sbcbii 3088

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 3087	. 2 |- ( T. -> ( [. A / x ]. ph <-> [. A / x ]. ps ) )
4	3	mptru 1404	1 |- ( [. A / x ]. ph <-> [. A / x ]. ps )

Syntax hints:   <-> wb 105   T. wtru 1396   [.wsbc 3028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-sbc 3029

This theorem is referenced by:  eqsbc2  3089  sbc3an  3090  sbccomlem  3103  sbccom  3104  sbcabel  3111  csbco  3134  csbcow  3135  sbcnel12g  3141  sbcne12g  3142  sbccsbg  3153  sbccsb2g  3154  csbnestgf  3177  csbabg  3186  sbcssg  3600  sbcrel  4804  difopab  4854  sbcfung  5341  f1od2  6379  mpoxopovel  6385  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmain  12514