Theorem sbcbii 3822

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766

This theorem is referenced by:  eqsbc2  3829  sbc3an  3830  sbccomlemOLD  3845  sbccom  3846  sbcrext  3848  sbcabel  3853  csbcow  3889  csbco  3890  sbcnel12g  4389  sbcne12  4390  csbcom  4395  csbnestgfw  4397  csbnestgf  4402  sbccsb  4411  sbccsb2  4412  csbab  4415  2nreu  4419  sbcssg  4495  sbcop  5464  sbcrel  5759  difopabOLD  5810  sbcfung  6559  tfinds2  7857  frpoins3xpg  8137  frpoins3xp3g  8138  mpoxopovel  8217  f1od2  32644  bnj62  34697  bnj89  34698  bnj156  34705  bnj524  34714  bnj610  34724  bnj919  34744  bnj976  34754  bnj110  34835  bnj91  34838  bnj92  34839  bnj106  34845  bnj121  34847  bnj124  34848  bnj125  34849  bnj126  34850  bnj130  34851  bnj154  34855  bnj155  34856  bnj153  34857  bnj207  34858  bnj523  34864  bnj526  34865  bnj539  34868  bnj540  34869  bnj581  34885  bnj591  34888  bnj609  34894  bnj611  34895  bnj934  34912  bnj1000  34918  bnj984  34929  bnj985v  34930  bnj985  34931  bnj1040  34949  bnj1123  34963  bnj1452  35029  bnj1463  35032  sbcalf  38084  sbcexf  38085  sbccom2lem  38094  sbccom2  38095  sbccom2f  38096  sbccom2fi  38097  csbcom2fi  38098  rspcsbnea  42090  2sbcrex  42754  2sbcrexOLD  42756  sbcrot3  42761  sbcrot5  42762  2rexfrabdioph  42766  3rexfrabdioph  42767  4rexfrabdioph  42768  6rexfrabdioph  42769  7rexfrabdioph  42770  rmydioph  42985  expdiophlem2  42993  sbcheg  43750  sbc3or  44505  trsbc  44513  onfrALTlem5  44515  eqsbc2VD  44812  sbcoreleleqVD  44831  onfrALTlem5VD  44857  ich2exprop  47433