Theorem sbcbii 3795

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

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1571  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3740

This theorem is used by:  eqsbc2  3802  sbc3an  3803  sbccom  3818  sbcrext  3820  sbcabel  3825  csbcow  3862  csbco  3863  sbcnel12g  4372  sbcne12  4373  csbcom  4378  csbnestgfw  4380  csbnestgf  4385  sbccsb  4394  sbccsb2  4395  csbab  4398  2nreu  4402  sbcssg  4477  sbcop  5459  sbcrel  5757  sbcfung  6555  sbcfungOLD  6556  tfinds2  7864  frpoins3xpg  8141  frpoins3xp3g  8142  mpoxopovel  8221  f1od2  33293  bnj62  35334  bnj89  35335  bnj156  35342  bnj524  35351  bnj610  35361  bnj919  35381  bnj976  35391  bnj110  35471  bnj91  35474  bnj92  35475  bnj106  35481  bnj121  35483  bnj124  35484  bnj125  35485  bnj126  35486  bnj130  35487  bnj154  35491  bnj155  35492  bnj153  35493  bnj207  35494  bnj523  35500  bnj526  35501  bnj539  35504  bnj540  35505  bnj581  35521  bnj591  35524  bnj609  35530  bnj611  35531  bnj934  35548  bnj1000  35554  bnj984  35565  bnj985v  35566  bnj985  35567  bnj1040  35585  bnj1123  35599  bnj1452  35665  bnj1463  35668  sbcalf  39014  sbcexf  39015  sbccom2lem  39024  sbccom2  39025  sbccom2f  39026  sbccom2fi  39027  csbcom2fi  39028  rspcsbnea  43149  2sbcrex  43748  sbcrot3  43751  sbcrot5  43752  2rexfrabdioph  43756  3rexfrabdioph  43757  4rexfrabdioph  43758  6rexfrabdioph  43759  7rexfrabdioph  43760  rmydioph  43974  expdiophlem2  43982  sbcheg  44738  sbc3or  45474  trsbc  45482  onfrALTlem5  45484  eqsbc2VD  45781  sbcoreleleqVD  45800  onfrALTlem5VD  45826  ich2exprop  48497