Theorem sbcbii 3813

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

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

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 3757

This theorem is referenced by:  eqsbc2  3820  sbc3an  3821  sbccomlemOLD  3836  sbccom  3837  sbcrext  3839  sbcabel  3844  csbcow  3880  csbco  3881  sbcnel12g  4380  sbcne12  4381  csbcom  4386  csbnestgfw  4388  csbnestgf  4393  sbccsb  4402  sbccsb2  4403  csbab  4406  2nreu  4410  sbcssg  4486  sbcop  5452  sbcrel  5746  difopabOLD  5797  sbcfung  6543  tfinds2  7843  frpoins3xpg  8122  frpoins3xp3g  8123  mpoxopovel  8202  f1od2  32651  bnj62  34717  bnj89  34718  bnj156  34725  bnj524  34734  bnj610  34744  bnj919  34764  bnj976  34774  bnj110  34855  bnj91  34858  bnj92  34859  bnj106  34865  bnj121  34867  bnj124  34868  bnj125  34869  bnj126  34870  bnj130  34871  bnj154  34875  bnj155  34876  bnj153  34877  bnj207  34878  bnj523  34884  bnj526  34885  bnj539  34888  bnj540  34889  bnj581  34905  bnj591  34908  bnj609  34914  bnj611  34915  bnj934  34932  bnj1000  34938  bnj984  34949  bnj985v  34950  bnj985  34951  bnj1040  34969  bnj1123  34983  bnj1452  35049  bnj1463  35052  sbcalf  38115  sbcexf  38116  sbccom2lem  38125  sbccom2  38126  sbccom2f  38127  sbccom2fi  38128  csbcom2fi  38129  rspcsbnea  42126  2sbcrex  42779  2sbcrexOLD  42781  sbcrot3  42786  sbcrot5  42787  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  rmydioph  43010  expdiophlem2  43018  sbcheg  43775  sbc3or  44529  trsbc  44537  onfrALTlem5  44539  eqsbc2VD  44836  sbcoreleleqVD  44855  onfrALTlem5VD  44881  ich2exprop  47476