Theorem sbcbii 3373

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

Syntax hints:   <-> wb 184   T. wtru 1384   [.wsbc 3313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-sbc 3314

This theorem is referenced by:  sbcbiiOLD  3374  eqsbc3r  3375  sbc3an  3376  sbccomlem  3392  sbccom  3393  sbcrextOLD  3395  sbcrext  3396  sbcabel  3402  csbco  3430  sbcnel12g  3812  sbcne12  3813  sbcne12gOLD  3814  csbcom  3823  csbnestgf  3826  sbccsb  3835  sbccsbgOLD  3836  sbccsb2  3837  sbccsb2gOLD  3838  csbab  3841  csbabgOLD  3842  sbcssg  3925  sbcrel  5079  difopab  5124  sbcfung  5601  tfinds2  6683  mpt2xopovel  6950  f1od2  27419  sbcalf  30492  sbcexf  30493  sbccom2lem  30504  sbccom2  30505  sbccom2f  30506  sbccom2fi  30507  csbcom2fi  30509  2sbcrex  30693  2sbcrexOLD  30694  sbcrot3  30699  sbcrot5  30700  2rexfrabdioph  30704  3rexfrabdioph  30705  4rexfrabdioph  30706  6rexfrabdioph  30707  7rexfrabdioph  30708  rmydioph  30931  expdiophlem2  30939  sbc3or  33035  trsbc  33044  onfrALTlem5  33047  bnj62  33506  bnj89  33507  bnj156  33516  bnj524  33526  bnj538OLD  33530  bnj610  33537  bnj919  33558  bnj976  33569  bnj110  33649  bnj91  33652  bnj92  33653  bnj106  33659  bnj121  33661  bnj124  33662  bnj125  33663  bnj126  33664  bnj130  33665  bnj154  33669  bnj155  33670  bnj153  33671  bnj207  33672  bnj523  33678  bnj526  33679  bnj539  33682  bnj540  33683  bnj581  33699  bnj591  33702  bnj609  33708  bnj611  33709  bnj934  33726  bnj1000  33732  bnj984  33743  bnj985  33744  bnj1040  33761  bnj1123  33775  bnj1452  33841  bnj1463  33844