Theorem sbcbii 3380

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

Syntax hints:   <-> wb 184   T. wtru 1399   [.wsbc 3324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3325

This theorem is referenced by:  eqsbc3r  3381  sbc3an  3382  sbccomlem  3395  sbccom  3396  sbcrext  3398  sbcabel  3402  csbco  3430  sbcnel12g  3824  sbcne12  3825  csbcom  3833  csbnestgf  3835  sbccsb  3843  sbccsb2  3844  csbab  3847  sbcssg  3928  sbcrel  5077  difopab  5123  sbcfung  5593  tfinds2  6671  mpt2xopovel  6940  f1od2  27778  sbcalf  30757  sbcexf  30758  sbccom2lem  30769  sbccom2  30770  sbccom2f  30771  sbccom2fi  30772  csbcom2fi  30774  2sbcrex  30957  2sbcrexOLD  30959  sbcrot3  30964  sbcrot5  30965  2rexfrabdioph  30969  3rexfrabdioph  30970  4rexfrabdioph  30971  6rexfrabdioph  30972  7rexfrabdioph  30973  rmydioph  31195  expdiophlem2  31203  sbc3or  33689  sbcbiiOLD  33692  trsbc  33701  onfrALTlem5  33708  csbabgOLD  34015  bnj62  34174  bnj89  34175  bnj156  34184  bnj524  34194  bnj538OLD  34198  bnj610  34205  bnj919  34226  bnj976  34237  bnj110  34317  bnj91  34320  bnj92  34321  bnj106  34327  bnj121  34329  bnj124  34330  bnj125  34331  bnj126  34332  bnj130  34333  bnj154  34337  bnj155  34338  bnj153  34339  bnj207  34340  bnj523  34346  bnj526  34347  bnj539  34350  bnj540  34351  bnj581  34367  bnj591  34370  bnj609  34376  bnj611  34377  bnj934  34394  bnj1000  34400  bnj984  34411  bnj985  34412  bnj1040  34429  bnj1123  34443  bnj1452  34509  bnj1463  34512