Theorem sbcbii 3801

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

Syntax hints:   ↔ wb 209  ⊤wtru 1571  [wsbc 3745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746

This theorem is referenced by:  eqsbc2  3808  sbc3an  3809  sbccomlemOLD  3824  sbccom  3825  sbcrext  3827  sbcabel  3832  csbcow  3869  csbco  3870  sbcnel12g  4380  sbcne12  4381  csbcom  4386  csbnestgfw  4388  csbnestgf  4393  sbccsb  4402  sbccsb2  4403  csbab  4406  2nreu  4410  sbcssg  4483  sbcop  5473  sbcrel  5769  sbcfung  6562  tfinds2  7861  frpoins3xpg  8137  frpoins3xp3g  8138  mpoxopovel  8217  f1od2  33045  bnj62  35090  bnj89  35091  bnj156  35098  bnj524  35107  bnj610  35117  bnj919  35137  bnj976  35147  bnj110  35227  bnj91  35230  bnj92  35231  bnj106  35237  bnj121  35239  bnj124  35240  bnj125  35241  bnj126  35242  bnj130  35243  bnj154  35247  bnj155  35248  bnj153  35249  bnj207  35250  bnj523  35256  bnj526  35257  bnj539  35260  bnj540  35261  bnj581  35277  bnj591  35280  bnj609  35286  bnj611  35287  bnj934  35304  bnj1000  35310  bnj984  35321  bnj985v  35322  bnj985  35323  bnj1040  35341  bnj1123  35355  bnj1452  35421  bnj1463  35424  sbcalf  38744  sbcexf  38745  sbccom2lem  38754  sbccom2  38755  sbccom2f  38756  sbccom2fi  38757  csbcom2fi  38758  rspcsbnea  42879  2sbcrex  43498  sbcrot3  43501  sbcrot5  43502  2rexfrabdioph  43506  3rexfrabdioph  43507  4rexfrabdioph  43508  6rexfrabdioph  43509  7rexfrabdioph  43510  rmydioph  43724  expdiophlem2  43732  sbcheg  44488  sbc3or  45224  trsbc  45232  onfrALTlem5  45234  eqsbc2VD  45531  sbcoreleleqVD  45550  onfrALTlem5VD  45576  ich2exprop  48203