Theorem sbcbii 3524

Description: Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.)

Hypothesis

Ref	Expression
sbcbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
sbcbii	⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

Proof of Theorem sbcbii

Step	Hyp	Ref	Expression
1		sbcbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	sbcbidv 3523	. 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
4	3	trud 1533	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

Syntax hints:   ↔ wb 196  ⊤wtru 1524  [wsbc 3468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-sbc 3469

This theorem is referenced by:  eqsbc3r  3525  eqsbc3rOLD  3526  sbc3an  3527  sbccomlem  3541  sbccom  3542  sbcrext  3544  sbcrextOLD  3545  sbcabel  3550  csbco  3576  sbcnel12g  4018  sbcne12  4019  csbcom  4027  csbnestgf  4029  sbccsb  4037  sbccsb2  4038  csbab  4041  sbcssg  4118  sbcrel  5239  difopab  5286  sbcfung  5950  tfinds2  7105  mpt2xopovel  7391  f1od2  29627  bnj62  30914  bnj89  30915  bnj156  30922  bnj524  30932  bnj538OLD  30936  bnj610  30943  bnj919  30963  bnj976  30974  bnj110  31054  bnj91  31057  bnj92  31058  bnj106  31064  bnj121  31066  bnj124  31067  bnj125  31068  bnj126  31069  bnj130  31070  bnj154  31074  bnj155  31075  bnj153  31076  bnj207  31077  bnj523  31083  bnj526  31084  bnj539  31087  bnj540  31088  bnj581  31104  bnj591  31107  bnj609  31113  bnj611  31114  bnj934  31131  bnj1000  31137  bnj984  31148  bnj985  31149  bnj1040  31166  bnj1123  31180  bnj1452  31246  bnj1463  31249  sbcalf  34047  sbcexf  34048  sbccom2lem  34059  sbccom2  34060  sbccom2f  34061  sbccom2fi  34062  csbcom2fi  34064  2sbcrex  37665  2sbcrexOLD  37667  sbcrot3  37672  sbcrot5  37673  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  rmydioph  37898  expdiophlem2  37906  sbcheg  38390  sbc3or  39055  sbcbiiOLD  39058  sbc3orgOLD  39059  trsbc  39067  sbcssOLD  39073  onfrALTlem5  39074  csbabgOLD  39367  onfrALTlem5VD  39435