Theorem sbcbii 3089

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 3088	. 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 3029

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 3030

This theorem is referenced by:  eqsbc2  3090  sbc3an  3091  sbccomlem  3104  sbccom  3105  sbcabel  3112  csbco  3135  csbcow  3136  sbcnel12g  3142  sbcne12g  3143  sbccsbg  3154  sbccsb2g  3155  csbnestgf  3178  csbabg  3187  sbcssg  3601  sbcrel  4810  difopab  4861  sbcfung  5348  f1od2  6395  mpoxopovel  6402  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemmain  12559