Theorem sbcbii 3865

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

Syntax hints:   ↔ wb 206  ⊤wtru 1538  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805

This theorem is referenced by:  eqsbc2  3873  sbc3an  3874  sbccomlemOLD  3892  sbccom  3893  sbcrext  3895  sbcabel  3900  csbcow  3936  csbco  3937  sbcnel12g  4437  sbcne12  4438  csbcom  4443  csbnestgfw  4445  csbnestgf  4450  sbccsb  4459  sbccsb2  4460  csbab  4463  2nreu  4467  sbcssg  4543  sbcop  5509  sbcrel  5804  difopabOLD  5855  sbcfung  6602  tfinds2  7901  frpoins3xpg  8181  frpoins3xp3g  8182  mpoxopovel  8261  f1od2  32735  bnj62  34696  bnj89  34697  bnj156  34704  bnj524  34713  bnj610  34723  bnj919  34743  bnj976  34753  bnj110  34834  bnj91  34837  bnj92  34838  bnj106  34844  bnj121  34846  bnj124  34847  bnj125  34848  bnj126  34849  bnj130  34850  bnj154  34854  bnj155  34855  bnj153  34856  bnj207  34857  bnj523  34863  bnj526  34864  bnj539  34867  bnj540  34868  bnj581  34884  bnj591  34887  bnj609  34893  bnj611  34894  bnj934  34911  bnj1000  34917  bnj984  34928  bnj985v  34929  bnj985  34930  bnj1040  34948  bnj1123  34962  bnj1452  35028  bnj1463  35031  sbcalf  38074  sbcexf  38075  sbccom2lem  38084  sbccom2  38085  sbccom2f  38086  sbccom2fi  38087  csbcom2fi  38088  rspcsbnea  42088  2sbcrex  42740  2sbcrexOLD  42742  sbcrot3  42747  sbcrot5  42748  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  rmydioph  42971  expdiophlem2  42979  sbcheg  43741  sbc3or  44503  trsbc  44511  onfrALTlem5  44513  eqsbc2VD  44811  sbcoreleleqVD  44830  onfrALTlem5VD  44856  ich2exprop  47345