Theorem sbcbii 3810

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

Syntax hints:   ↔ wb 206  ⊤wtru 1541  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3754

This theorem is referenced by:  eqsbc2  3817  sbc3an  3818  sbccomlemOLD  3833  sbccom  3834  sbcrext  3836  sbcabel  3841  csbcow  3877  csbco  3878  sbcnel12g  4377  sbcne12  4378  csbcom  4383  csbnestgfw  4385  csbnestgf  4390  sbccsb  4399  sbccsb2  4400  csbab  4403  2nreu  4407  sbcssg  4483  sbcop  5449  sbcrel  5743  difopabOLD  5794  sbcfung  6540  tfinds2  7840  frpoins3xpg  8119  frpoins3xp3g  8120  mpoxopovel  8199  f1od2  32644  bnj62  34710  bnj89  34711  bnj156  34718  bnj524  34727  bnj610  34737  bnj919  34757  bnj976  34767  bnj110  34848  bnj91  34851  bnj92  34852  bnj106  34858  bnj121  34860  bnj124  34861  bnj125  34862  bnj126  34863  bnj130  34864  bnj154  34868  bnj155  34869  bnj153  34870  bnj207  34871  bnj523  34877  bnj526  34878  bnj539  34881  bnj540  34882  bnj581  34898  bnj591  34901  bnj609  34907  bnj611  34908  bnj934  34925  bnj1000  34931  bnj984  34942  bnj985v  34943  bnj985  34944  bnj1040  34962  bnj1123  34976  bnj1452  35042  bnj1463  35045  sbcalf  38108  sbcexf  38109  sbccom2lem  38118  sbccom2  38119  sbccom2f  38120  sbccom2fi  38121  csbcom2fi  38122  rspcsbnea  42119  2sbcrex  42772  2sbcrexOLD  42774  sbcrot3  42779  sbcrot5  42780  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  rmydioph  43003  expdiophlem2  43011  sbcheg  43768  sbc3or  44522  trsbc  44530  onfrALTlem5  44532  eqsbc2VD  44829  sbcoreleleqVD  44848  onfrALTlem5VD  44874  ich2exprop  47472