Theorem sbcbii 3812

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3756

This theorem is referenced by:  eqsbc2  3819  sbc3an  3820  sbccomlemOLD  3835  sbccom  3836  sbcrext  3838  sbcabel  3843  csbcow  3879  csbco  3880  sbcnel12g  4379  sbcne12  4380  csbcom  4385  csbnestgfw  4387  csbnestgf  4392  sbccsb  4401  sbccsb2  4402  csbab  4405  2nreu  4409  sbcssg  4485  sbcop  5451  sbcrel  5745  difopabOLD  5796  sbcfung  6542  tfinds2  7842  frpoins3xpg  8121  frpoins3xp3g  8122  mpoxopovel  8201  f1od2  32650  bnj62  34716  bnj89  34717  bnj156  34724  bnj524  34733  bnj610  34743  bnj919  34763  bnj976  34773  bnj110  34854  bnj91  34857  bnj92  34858  bnj106  34864  bnj121  34866  bnj124  34867  bnj125  34868  bnj126  34869  bnj130  34870  bnj154  34874  bnj155  34875  bnj153  34876  bnj207  34877  bnj523  34883  bnj526  34884  bnj539  34887  bnj540  34888  bnj581  34904  bnj591  34907  bnj609  34913  bnj611  34914  bnj934  34931  bnj1000  34937  bnj984  34948  bnj985v  34949  bnj985  34950  bnj1040  34968  bnj1123  34982  bnj1452  35048  bnj1463  35051  sbcalf  38103  sbcexf  38104  sbccom2lem  38113  sbccom2  38114  sbccom2f  38115  sbccom2fi  38116  csbcom2fi  38117  rspcsbnea  42114  2sbcrex  42765  2sbcrexOLD  42767  sbcrot3  42772  sbcrot5  42773  2rexfrabdioph  42777  3rexfrabdioph  42778  4rexfrabdioph  42779  6rexfrabdioph  42780  7rexfrabdioph  42781  rmydioph  42996  expdiophlem2  43004  sbcheg  43761  sbc3or  44515  trsbc  44523  onfrALTlem5  44525  eqsbc2VD  44822  sbcoreleleqVD  44841  onfrALTlem5VD  44867  ich2exprop  47462