Theorem sbcbii 3102

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

Syntax hints:   <-> wb 105   T. wtru 1399   [.wsbc 3042

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-sbc 3043

This theorem is referenced by:  eqsbc2  3103  sbc3an  3104  sbccomlem  3117  sbccom  3118  sbcabel  3125  csbco  3148  csbcow  3149  sbcnel12g  3155  sbcne12g  3156  sbccsbg  3167  sbccsb2g  3168  csbnestgf  3191  csbabg  3200  sbcssg  3618  sbcrel  4836  difopab  4888  sbcfung  5376  f1od2  6431  mpoxopovel  6472  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemmain  12694