Theorem sbcbii 3786

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 3785	. 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
4	3	mptru 1554	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

Syntax hints:   ↔ wb 207  ⊤wtru 1548  [wsbc 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-sbc 3731

This theorem is referenced by:  eqsbc2  3793  sbc3an  3794  sbccomlemOLD  3809  sbccom  3810  sbcrext  3812  sbcabel  3817  csbcow  3853  csbco  3854  sbcnel12g  4349  sbcne12  4350  csbcom  4355  csbnestgfw  4357  csbnestgf  4362  sbccsb  4371  sbccsb2  4372  csbab  4375  2nreu  4379  sbcssg  4456  sbcop  5436  sbcrel  5731  sbcfung  6516  tfinds2  7811  frpoins3xpg  8087  frpoins3xp3g  8088  mpoxopovel  8167  f1od2  32818  bnj62  34910  bnj89  34911  bnj156  34918  bnj524  34927  bnj610  34937  bnj919  34957  bnj976  34967  bnj110  35047  bnj91  35050  bnj92  35051  bnj106  35057  bnj121  35059  bnj124  35060  bnj125  35061  bnj126  35062  bnj130  35063  bnj154  35067  bnj155  35068  bnj153  35069  bnj207  35070  bnj523  35076  bnj526  35077  bnj539  35080  bnj540  35081  bnj581  35097  bnj591  35100  bnj609  35106  bnj611  35107  bnj934  35124  bnj1000  35130  bnj984  35141  bnj985v  35142  bnj985  35143  bnj1040  35161  bnj1123  35175  bnj1452  35241  bnj1463  35244  sbcalf  38488  sbcexf  38489  sbccom2lem  38498  sbccom2  38499  sbccom2f  38500  sbccom2fi  38501  csbcom2fi  38502  rspcsbnea  42623  2sbcrex  43240  sbcrot3  43243  sbcrot5  43244  2rexfrabdioph  43248  3rexfrabdioph  43249  4rexfrabdioph  43250  6rexfrabdioph  43251  7rexfrabdioph  43252  rmydioph  43466  expdiophlem2  43474  sbcheg  44230  sbc3or  44983  trsbc  44991  onfrALTlem5  44993  eqsbc2VD  45290  sbcoreleleqVD  45309  onfrALTlem5VD  45335  ich2exprop  47953