Theorem sbcbii 3797

Description: Formula-building inference 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 3796	. 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
4	3	mptru 1548	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

Syntax hints:   ↔ wb 206  ⊤wtru 1542  [wsbc 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3741

This theorem is referenced by:  eqsbc2  3804  sbc3an  3805  sbccomlemOLD  3820  sbccom  3821  sbcrext  3823  sbcabel  3828  csbcow  3864  csbco  3865  sbcnel12g  4366  sbcne12  4367  csbcom  4372  csbnestgfw  4374  csbnestgf  4379  sbccsb  4388  sbccsb2  4389  csbab  4392  2nreu  4396  sbcssg  4474  sbcop  5437  sbcrel  5730  sbcfung  6516  tfinds2  7806  frpoins3xpg  8082  frpoins3xp3g  8083  mpoxopovel  8162  f1od2  32798  bnj62  34876  bnj89  34877  bnj156  34884  bnj524  34893  bnj610  34903  bnj919  34923  bnj976  34933  bnj110  35014  bnj91  35017  bnj92  35018  bnj106  35024  bnj121  35026  bnj124  35027  bnj125  35028  bnj126  35029  bnj130  35030  bnj154  35034  bnj155  35035  bnj153  35036  bnj207  35037  bnj523  35043  bnj526  35044  bnj539  35047  bnj540  35048  bnj581  35064  bnj591  35067  bnj609  35073  bnj611  35074  bnj934  35091  bnj1000  35097  bnj984  35108  bnj985v  35109  bnj985  35110  bnj1040  35128  bnj1123  35142  bnj1452  35208  bnj1463  35211  sbcalf  38315  sbcexf  38316  sbccom2lem  38325  sbccom2  38326  sbccom2f  38327  sbccom2fi  38328  csbcom2fi  38329  rspcsbnea  42385  2sbcrex  43026  2sbcrexOLD  43028  sbcrot3  43033  sbcrot5  43034  2rexfrabdioph  43038  3rexfrabdioph  43039  4rexfrabdioph  43040  6rexfrabdioph  43041  7rexfrabdioph  43042  rmydioph  43256  expdiophlem2  43264  sbcheg  44020  sbc3or  44773  trsbc  44781  onfrALTlem5  44783  eqsbc2VD  45080  sbcoreleleqVD  45099  onfrALTlem5VD  45125  ich2exprop  47717