Theorem sbcbii 3799

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

Syntax hints:   ↔ wb 206  ⊤wtru 1543  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3743

This theorem is referenced by:  eqsbc2  3806  sbc3an  3807  sbccomlemOLD  3822  sbccom  3823  sbcrext  3825  sbcabel  3830  csbcow  3866  csbco  3867  sbcnel12g  4368  sbcne12  4369  csbcom  4374  csbnestgfw  4376  csbnestgf  4381  sbccsb  4390  sbccsb2  4391  csbab  4394  2nreu  4398  sbcssg  4476  sbcop  5445  sbcrel  5738  sbcfung  6524  tfinds2  7816  frpoins3xpg  8092  frpoins3xp3g  8093  mpoxopovel  8172  f1od2  32808  bnj62  34896  bnj89  34897  bnj156  34904  bnj524  34913  bnj610  34923  bnj919  34943  bnj976  34953  bnj110  35033  bnj91  35036  bnj92  35037  bnj106  35043  bnj121  35045  bnj124  35046  bnj125  35047  bnj126  35048  bnj130  35049  bnj154  35053  bnj155  35054  bnj153  35055  bnj207  35056  bnj523  35062  bnj526  35063  bnj539  35066  bnj540  35067  bnj581  35083  bnj591  35086  bnj609  35092  bnj611  35093  bnj934  35110  bnj1000  35116  bnj984  35127  bnj985v  35128  bnj985  35129  bnj1040  35147  bnj1123  35161  bnj1452  35227  bnj1463  35230  sbcalf  38362  sbcexf  38363  sbccom2lem  38372  sbccom2  38373  sbccom2f  38374  sbccom2fi  38375  csbcom2fi  38376  rspcsbnea  42498  2sbcrex  43138  2sbcrexOLD  43140  sbcrot3  43145  sbcrot5  43146  2rexfrabdioph  43150  3rexfrabdioph  43151  4rexfrabdioph  43152  6rexfrabdioph  43153  7rexfrabdioph  43154  rmydioph  43368  expdiophlem2  43376  sbcheg  44132  sbc3or  44885  trsbc  44893  onfrALTlem5  44895  eqsbc2VD  45192  sbcoreleleqVD  45211  onfrALTlem5VD  45237  ich2exprop  47828